Nuprl Lemma : vr_PEXT_implies_A_eq_AimpA
vr_PEXT 
(
P:
. (P ((P 
P) = P)))
Proof not projected
Definitions occuring in Statement :
vr_PEXT: vr_PEXT,
prop: ,
all: x:A. B[x],
implies: P Q,
function: x:A B[x],
equal: s = t
Definitions :
CollapseTHENA: Error :CollapseTHENA,
Unfold: Error :Unfold,
CollapseTHEN: Error :CollapseTHEN,
function: x:A B[x],
Auto: Error :Auto,
all: x:A. B[x],
equal: s = t,
member: t 
T,
universe: Type,
prop: ,
implies: P Q,
vr_PEXT: vr_PEXT,
iff: P 
Q,
and: P 
Q,
product: x:A 
B[x],
rev_implies: P Q
Lemmas :
vr_PEXT_wf
vr\_PEXT {}\mRightarrow{} (\mforall{}P:\mBbbP{}. (P {}\mRightarrow{} ((P {}\mrightarrow{} P) = P)))
Date html generated:
2012_02_20-PM-03_33_59
Last ObjectModification:
2012_02_02-PM-01_55_28
Home
Index