Nuprl Definition : vr_exists_uni
!x:T. P[x] == x:T. (P[x] 
(
y:T. (P[y] 
(x = y))))
Definitions occuring in Statement :
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
and: P Q,
equal: s = t
FDL editor aliases :
vr_exists_uni
\mexists{}!x:T. P[x] == \mexists{}x:T. (P[x] \mwedge{} (\mforall{}y:T. (P[y] {}\mRightarrow{} (x = y))))
Date html generated:
2012_02_20-PM-03_32_42
Last ObjectModification:
2012_02_02-PM-01_55_07
Home
Index