Nuprl Definition : exists_uni
∃!x:T. P[x] == ∃x:T. (P[x] ∧ (∀y:T. (P[y] ⇒ (x = y ∈ T))))
Definitions occuring in Statement :
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
equal: s = t ∈ T
Definitions occuring in definition :
exists: ∃x:A. B[x],
and: P ∧ Q,
all: ∀x:A. B[x],
implies: P ⇒ Q,
equal: s = t ∈ T
FDL editor aliases :
exists_uni
exists_uni
Latex:
\mexists{}!x:T. P[x] == \mexists{}x:T. (P[x] \mwedge{} (\mforall{}y:T. (P[y] {}\mRightarrow{} (x = y))))
Date html generated:
2016_05_15-PM-03_23_12
Last ObjectModification:
2015_09_23-AM-07_43_05
Theory : general
Home
Index