Nuprl Definition : existssetmem
∃a∈A.P[a] == ∃i:set-dom(A). P[set-item(A;i)]
Definitions occuring in Statement :
set-item: set-item(s;x),
set-dom: set-dom(s),
exists: ∃x:A. B[x]
Definitions occuring in definition :
set-item: set-item(s;x),
set-dom: set-dom(s),
exists: ∃x:A. B[x]
FDL editor aliases :
existssetmem
Latex:
\mexists{}a\mmember{}A.P[a] == \mexists{}i:set-dom(A). P[set-item(A;i)]
Date html generated:
2018_05_29-PM-01_48_23
Last ObjectModification:
2018_05_28-AM-11_03_57
Theory : constructive!set!theory
Home
Index