Nuprl Lemma : equipollent_functionality_wrt_equipollent2

[A,B1,B2:Type].  (B1 B2  (A B1 ⇐⇒ B2))


Proof




Definitions occuring in Statement :  equipollent: B uall: [x:A]. B[x] iff: ⇐⇒ Q implies:  Q universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] implies:  Q iff: ⇐⇒ Q and: P ∧ Q member: t ∈ T guard: {T} rev_implies:  Q
Lemmas referenced :  equipollent_transitivity equipollent_wf equipollent_inversion
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation independent_pairFormation cut hypothesis lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality independent_functionElimination universeEquality

Latex:
\mforall{}[A,B1,B2:Type].    (B1  \msim{}  B2  {}\mRightarrow{}  (A  \msim{}  B1  \mLeftarrow{}{}\mRightarrow{}  A  \msim{}  B2))



Date html generated: 2016_05_14-PM-04_00_19
Last ObjectModification: 2015_12_26-PM-07_44_16

Theory : equipollence!!cardinality!


Home Index