![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > p0ex | Structured version Visualization version GIF version |
Description: The power set of the empty set (the ordinal 1) is a set. See also p0exALT 5380. (Contributed by NM, 23-Dec-1993.) |
Ref | Expression |
---|---|
p0ex | ⊢ {∅} ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pw0 4812 | . 2 ⊢ 𝒫 ∅ = {∅} | |
2 | 0ex 5303 | . . 3 ⊢ ∅ ∈ V | |
3 | 2 | pwex 5375 | . 2 ⊢ 𝒫 ∅ ∈ V |
4 | 1, 3 | eqeltrri 2823 | 1 ⊢ {∅} ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2099 Vcvv 3463 ∅c0 4323 𝒫 cpw 4598 {csn 4624 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 ax-sep 5295 ax-nul 5302 ax-pow 5360 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-v 3465 df-dif 3950 df-ss 3964 df-nul 4324 df-pw 4600 df-sn 4625 |
This theorem is referenced by: pp0ex 5381 dtruALT 5383 zfpair 5416 tposexg 8245 fsetexb 8883 endisj 9086 pw2eng 9106 dfac4 10156 dfac2b 10164 axcc2lem 10468 axdc2lem 10480 axcclem 10489 axpowndlem3 10631 isstruct2 17144 cat1 18112 plusffval 18632 grpinvfval 18966 grpsubfval 18971 mulgfval 19057 0symgefmndeq 19385 staffval 20814 scaffval 20850 lpival 21307 ipffval 21638 refun0 23505 filconn 23873 alexsubALTlem2 24038 nmfval 24583 tcphex 25231 tchnmfval 25242 legval 28506 locfinref 33667 oms0 34142 bnj105 34580 ssoninhaus 36171 onint1 36172 bj-tagex 36705 bj-1uplex 36726 rrnval 37539 lsatset 38699 mnuprdlem2 43982 mnuprdlem3 43983 dvnprodlem3 45603 ioorrnopn 45960 ioorrnopnxr 45962 ismeannd 46122 |
Copyright terms: Public domain | W3C validator |