### Nuprl Lemma : equipollent_functionality_wrt_ext-eq-left

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

Proof

Definitions occuring in Statement :  equipollent: `A ~ B` ext-eq: `A ≡ B` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` iff: `P `⇐⇒` Q` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` uimplies: `b supposing a` member: `t ∈ T` ext-eq: `A ≡ B` and: `P ∧ Q` subtype_rel: `A ⊆r B` iff: `P `⇐⇒` Q` implies: `P `` Q` guard: `{T}` rev_implies: `P `` 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

Latex:
\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