### Nuprl Lemma : change-equality-type

`∀[A,B:Type].  (respects-equality(A;B) `` (∀x,y:A.  ((x = y ∈ A) `` (x ∈ B) `` (x = y ∈ B))))`

Proof

Definitions occuring in Statement :  respects-equality: `respects-equality(S;T)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` all: `∀x:A. B[x]` member: `t ∈ T` respects-equality: `respects-equality(S;T)`
Lemmas referenced :  respects-equality_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  Error :lambdaFormation_alt,  sqequalRule Error :equalityIstype,  Error :universeIsType,  hypothesisEquality cut hypothesis sqequalHypSubstitution dependent_functionElimination thin independent_functionElimination because_Cache introduction extract_by_obid isectElimination Error :inhabitedIsType,  universeEquality pointwiseFunctionalityForEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}[A,B:Type].    (respects-equality(A;B)  {}\mRightarrow{}  (\mforall{}x,y:A.    ((x  =  y)  {}\mRightarrow{}  (x  \mmember{}  B)  {}\mRightarrow{}  (x  =  y))))

Date html generated: 2019_06_20-AM-11_13_51
Last ObjectModification: 2018_11_28-PM-11_36_14

Theory : core_2

Home Index