Nuprl Definition : exists_uni_upto
(r)∃!x:T. Q[x] == ∃a:T. a r !x:T. Q[x]
Definitions occuring in Statement :
uni_sat_upto: uni_sat_upto,
exists: ∃x:A. B[x]
Definitions occuring in definition :
exists: ∃x:A. B[x],
uni_sat_upto: uni_sat_upto
Latex:
(r)\mexists{}!x:T. Q[x] == \mexists{}a:T. a r !x:T. Q[x]
Date html generated:
2016_05_16-AM-07_45_10
Last ObjectModification:
2015_09_23-AM-09_51_57
Theory : factor_1
Home
Index