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 4854. (Contributed by NM, 23-Dec-1993.) |
Ref | Expression |
---|---|
p0ex | ⊢ {∅} ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pw0 4343 | . 2 ⊢ 𝒫 ∅ = {∅} | |
2 | 0ex 4790 | . . 3 ⊢ ∅ ∈ V | |
3 | 2 | pwex 4848 | . 2 ⊢ 𝒫 ∅ ∈ V |
4 | 1, 3 | eqeltrri 2698 | 1 ⊢ {∅} ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 1990 Vcvv 3200 ∅c0 3915 𝒫 cpw 4158 {csn 4177 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-dif 3577 df-in 3581 df-ss 3588 df-nul 3916 df-pw 4160 df-sn 4178 |
This theorem is referenced by: pp0ex 4855 dtruALT 4899 zfpair 4904 opthprc 5167 snsn0non 5846 fvclex 7138 tposexg 7366 2dom 8029 map1 8036 endisj 8047 pw2eng 8066 dfac4 8945 dfac2 8953 cdaval 8992 axcc2lem 9258 axdc2lem 9270 axcclem 9279 axpowndlem3 9421 isstruct2 15867 plusffval 17247 staffval 18847 scaffval 18881 lpival 19245 ipffval 19993 refun0 21318 filconn 21687 alexsubALTlem2 21852 nmfval 22393 tchex 23016 tchnmfval 23027 legval 25479 locfinref 29908 oms0 30359 bnj105 30790 rankeq1o 32278 ssoninhaus 32447 onint1 32448 bj-tagex 32975 bj-1uplex 32996 rrnval 33626 lsatset 34277 dvnprodlem3 40163 ioorrnopn 40525 ioorrnopnxr 40527 ismeannd 40684 |
Copyright terms: Public domain | W3C validator |