Nuprl Lemma : cand_functionality_wrt_iff

`∀[a1,a2,b1,b2:ℙ].  ((a1 `⇐⇒` a2) `` (b1 `⇐⇒` b2) `` (a1 c∧ b1 `⇐⇒` a2 c∧ b2))`

Proof

Definitions occuring in Statement :  uall: `∀[x:A]. B[x]` cand: `A c∧ B` prop: `ℙ` iff: `P `⇐⇒` Q` implies: `P `` Q`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` cand: `A c∧ B` member: `t ∈ T` prop: `ℙ` rev_implies: `P `` Q`
Lemmas referenced :  iff_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt lambdaFormation sqequalHypSubstitution productElimination thin independent_pairFormation productEquality cumulativity hypothesisEquality cut introduction extract_by_obid isectElimination hypothesis inhabitedIsType universeIsType universeEquality independent_functionElimination

Latex:
\mforall{}[a1,a2,b1,b2:\mBbbP{}].    ((a1  \mLeftarrow{}{}\mRightarrow{}  a2)  {}\mRightarrow{}  (b1  \mLeftarrow{}{}\mRightarrow{}  b2)  {}\mRightarrow{}  (a1  c\mwedge{}  b1  \mLeftarrow{}{}\mRightarrow{}  a2  c\mwedge{}  b2))

Date html generated: 2019_10_15-AM-10_46_37
Last ObjectModification: 2018_09_27-AM-09_41_12

Theory : basic

Home Index