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 4780. (Contributed by NM, 23-Dec-1993.) |
Ref | Expression |
---|---|
p0ex | ⊢ {∅} ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pw0 4283 | . 2 ⊢ 𝒫 ∅ = {∅} | |
2 | 0ex 4718 | . . 3 ⊢ ∅ ∈ V | |
3 | 2 | pwex 4774 | . 2 ⊢ 𝒫 ∅ ∈ V |
4 | 1, 3 | eqeltrri 2685 | 1 ⊢ {∅} ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 1977 Vcvv 3173 ∅c0 3874 𝒫 cpw 4108 {csn 4125 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pow 4769 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-dif 3543 df-in 3547 df-ss 3554 df-nul 3875 df-pw 4110 df-sn 4126 |
This theorem is referenced by: pp0ex 4781 dtruALT 4826 zfpair 4831 opthprc 5089 snsn0non 5763 fvclex 7031 tposexg 7253 2dom 7915 map1 7921 endisj 7932 pw2eng 7951 dfac4 8828 dfac2 8836 cdaval 8875 axcc2lem 9141 axdc2lem 9153 axcclem 9162 axpowndlem3 9300 isstruct2 15704 plusffval 17070 staffval 18670 scaffval 18704 lpival 19066 ipffval 19812 refun0 21128 filcon 21497 alexsubALTlem2 21662 nmfval 22203 tchex 22824 tchnmfval 22835 legval 25279 locfinref 29236 oms0 29686 bnj105 30044 rankeq1o 31448 ssoninhaus 31617 onint1 31618 bj-tagex 32168 bj-1uplex 32189 rrnval 32796 lsatset 33295 dvnprodlem3 38838 ioorrnopn 39201 ioorrnopnxr 39203 ismeannd 39360 |
Copyright terms: Public domain | W3C validator |