![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > p0ex | GIF version |
Description: The power set of the empty set (the ordinal 1) is a set. (Contributed by NM, 23-Dec-1993.) |
Ref | Expression |
---|---|
p0ex | ⊢ {∅} ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pw0 3754 | . 2 ⊢ 𝒫 ∅ = {∅} | |
2 | 0ex 4145 | . . 3 ⊢ ∅ ∈ V | |
3 | 2 | pwex 4201 | . 2 ⊢ 𝒫 ∅ ∈ V |
4 | 1, 3 | eqeltrri 2263 | 1 ⊢ {∅} ∈ V |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 2160 Vcvv 2752 ∅c0 3437 𝒫 cpw 3590 {csn 3607 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-14 2163 ax-ext 2171 ax-sep 4136 ax-nul 4144 ax-pow 4192 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-v 2754 df-dif 3146 df-in 3150 df-ss 3157 df-nul 3438 df-pw 3592 df-sn 3613 |
This theorem is referenced by: pp0ex 4207 undifexmid 4211 exmidexmid 4214 exmidundif 4224 exmidundifim 4225 exmid1stab 4226 ordtriexmidlem 4536 ontr2exmid 4542 onsucsssucexmid 4544 onsucelsucexmid 4547 regexmidlemm 4549 ordsoexmid 4579 ordtri2or2exmid 4588 ontri2orexmidim 4589 opthprc 4695 acexmidlema 5887 acexmidlem2 5893 tposexg 6283 2dom 6831 map1 6838 endisj 6850 ssfiexmid 6904 domfiexmid 6906 exmidpw 6936 exmidpw2en 6940 djuex 7072 exmidomni 7170 exmidonfinlem 7222 exmidfodomrlemr 7231 exmidfodomrlemrALT 7232 exmidaclem 7237 pw1dom2 7256 pw1ne1 7258 sbthom 15236 |
Copyright terms: Public domain | W3C validator |