Nuprl Lemma : equipollent_functionality_wrt_ext-eq-left

[A1,A2,B1,B2:Type].  (A1 B1 ⇐⇒ A2 B2) supposing ((B1 B2 ∈ Type) and A1 ≡ A2)


Definitions occuring in Statement :  equipollent: B ext-eq: A ≡ B uimplies: supposing a uall: [x:A]. B[x] iff: ⇐⇒ Q universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] uimplies: supposing a member: t ∈ T ext-eq: A ≡ B and: P ∧ Q subtype_rel: A ⊆B iff: ⇐⇒ Q implies:  Q guard: {T} rev_implies:  Q prop:
Lemmas referenced :  equipollent_functionality_wrt_ext-eq ext-eq_weakening equipollent_wf equal_wf ext-eq_wf equipollent_transitivity equipollent_weakening_ext-eq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut introduction sqequalRule sqequalHypSubstitution productElimination thin independent_pairEquality axiomEquality hypothesis rename independent_pairFormation lambdaFormation lemma_by_obid isectElimination hypothesisEquality independent_isectElimination independent_functionElimination instantiate universeEquality because_Cache equalitySymmetry

\mforall{}[A1,A2,B1,B2:Type].    (A1  \msim{}  B1  \mLeftarrow{}{}\mRightarrow{}  A2  \msim{}  B2)  supposing  ((B1  =  B2)  and  A1  \mequiv{}  A2)

Date html generated: 2016_05_14-PM-04_00_18
Last ObjectModification: 2015_12_26-PM-07_44_29

Theory : equipollence!!cardinality!

Home Index