### Nuprl Lemma : union_functionality_wrt_uiff2

[P1,P2,Q1,Q2:ℙ].  ({uiff(P1;P2)}  (Q1 Q2 ∈ ℙ {P1 Q1 ⇐⇒ P2 Q2})

Proof

Definitions occuring in Statement :  uiff: uiff(P;Q) uall: [x:A]. B[x] prop: guard: {T} iff: ⇐⇒ Q implies:  Q union: left right equal: t ∈ T
Definitions unfolded in proof :  guard: {T} or: P ∨ Q uall: [x:A]. B[x] implies:  Q uiff: uiff(P;Q) and: P ∧ Q iff: ⇐⇒ Q uimplies: supposing a member: t ∈ T prop: rev_implies:  Q
Lemmas referenced :  or_wf equal_wf uiff_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep Error :isect_memberFormation_alt,  lambdaFormation sqequalHypSubstitution productElimination thin independent_pairFormation unionElimination inlFormation independent_isectElimination hypothesis hypothesisEquality inrFormation cut hyp_replacement equalitySymmetry introduction extract_by_obid isectElimination instantiate universeEquality Error :inhabitedIsType,  Error :universeIsType

Latex:
\mforall{}[P1,P2,Q1,Q2:\mBbbP{}].    (\{uiff(P1;P2)\}  {}\mRightarrow{}  (Q1  =  Q2)  {}\mRightarrow{}  \{P1  +  Q1  \mLeftarrow{}{}\mRightarrow{}  P2  +  Q2\})

Date html generated: 2019_06_20-AM-11_17_25
Last ObjectModification: 2018_09_26-AM-10_24_49

Theory : core_2

Home Index