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: P ⇐⇒ Q,
implies: P ⇒ Q
Definitions unfolded in proof :
guard: {T},
all: ∀x:A. B[x],
implies: P ⇒ 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