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 5276. (Contributed by NM, 23-Dec-1993.) |
Ref | Expression |
---|---|
p0ex | ⊢ {∅} ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pw0 4737 | . 2 ⊢ 𝒫 ∅ = {∅} | |
2 | 0ex 5202 | . . 3 ⊢ ∅ ∈ V | |
3 | 2 | pwex 5272 | . 2 ⊢ 𝒫 ∅ ∈ V |
4 | 1, 3 | eqeltrri 2907 | 1 ⊢ {∅} ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2105 Vcvv 3492 ∅c0 4288 𝒫 cpw 4535 {csn 4557 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-sep 5194 ax-nul 5201 ax-pow 5257 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-v 3494 df-dif 3936 df-in 3940 df-ss 3949 df-nul 4289 df-pw 4537 df-sn 4558 |
This theorem is referenced by: pp0ex 5277 dtruALT 5279 zfpair 5312 tposexg 7895 endisj 8592 pw2eng 8611 dfac4 9536 dfac2b 9544 axcc2lem 9846 axdc2lem 9858 axcclem 9867 axpowndlem3 10009 isstruct2 16481 plusffval 17846 grpinvfval 18080 grpsubfval 18085 mulgfval 18164 staffval 19547 scaffval 19581 lpival 19946 ipffval 20720 refun0 22051 filconn 22419 alexsubALTlem2 22584 nmfval 23125 tcphex 23747 tchnmfval 23758 legval 26297 locfinref 31004 oms0 31454 bnj105 31893 ssoninhaus 33693 onint1 33694 bj-tagex 34196 bj-1uplex 34217 rrnval 34986 lsatset 36006 mnuprdlem2 40486 mnuprdlem3 40487 dvnprodlem3 42109 ioorrnopn 42467 ioorrnopnxr 42469 ismeannd 42626 |
Copyright terms: Public domain | W3C validator |