![]() |
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 5084. (Contributed by NM, 23-Dec-1993.) |
Ref | Expression |
---|---|
p0ex | ⊢ {∅} ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pw0 4561 | . 2 ⊢ 𝒫 ∅ = {∅} | |
2 | 0ex 5014 | . . 3 ⊢ ∅ ∈ V | |
3 | 2 | pwex 5080 | . 2 ⊢ 𝒫 ∅ ∈ V |
4 | 1, 3 | eqeltrri 2903 | 1 ⊢ {∅} ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2166 Vcvv 3414 ∅c0 4144 𝒫 cpw 4378 {csn 4397 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2803 ax-sep 5005 ax-nul 5013 ax-pow 5065 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-v 3416 df-dif 3801 df-in 3805 df-ss 3812 df-nul 4145 df-pw 4380 df-sn 4398 |
This theorem is referenced by: pp0ex 5085 dtruALT 5087 zfpair 5125 opthprc 5400 snsn0non 6081 fvclex 7400 tposexg 7631 2dom 8295 endisj 8316 pw2eng 8335 dfac4 9258 dfac2b 9266 dfac2OLD 9268 cdaval 9307 axcc2lem 9573 axdc2lem 9585 axcclem 9594 axpowndlem3 9736 isstruct2 16232 plusffval 17600 staffval 19203 scaffval 19237 lpival 19606 ipffval 20355 refun0 21689 filconn 22057 alexsubALTlem2 22222 nmfval 22763 tcphex 23385 tchnmfval 23396 legval 25896 locfinref 30453 oms0 30904 bnj105 31339 ssoninhaus 32980 onint1 32981 bj-tagex 33497 bj-1uplex 33518 lindsadd 33946 rrnval 34168 lsatset 35065 dvnprodlem3 40958 ioorrnopn 41316 ioorrnopnxr 41318 ismeannd 41475 |
Copyright terms: Public domain | W3C validator |