Nuprl Lemma : guard_functionality_wrt_iff

p,q:ℙ.  ({p ⇐⇒ q}  {{p} ⇐⇒ {q}})


Proof




Definitions occuring in Statement :  prop: guard: {T} all: x:A. B[x] iff: ⇐⇒ Q implies:  Q
Definitions unfolded in proof :  guard: {T} all: x:A. B[x] implies:  Q member: t ∈ T prop: uall: [x:A]. B[x]

Latex:
\mforall{}p,q:\mBbbP{}.    (\{p  \mLeftarrow{}{}\mRightarrow{}  q\}  {}\mRightarrow{}  \{\{p\}  \mLeftarrow{}{}\mRightarrow{}  \{q\}\})



Date html generated: 2016_05_17-AM-10_07_17
Last ObjectModification: 2015_12_29-PM-03_51_01

Theory : classrel!lemmas


Home Index