| 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 5385. (Contributed by NM, 23-Dec-1993.) |
| Ref | Expression |
|---|---|
| p0ex | ⊢ {∅} ∈ V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pw0 4812 | . 2 ⊢ 𝒫 ∅ = {∅} | |
| 2 | 0ex 5307 | . . 3 ⊢ ∅ ∈ V | |
| 3 | 2 | pwex 5380 | . 2 ⊢ 𝒫 ∅ ∈ V |
| 4 | 1, 3 | eqeltrri 2838 | 1 ⊢ {∅} ∈ V |
| Colors of variables: wff setvar class |
| Syntax hints: ∈ wcel 2108 Vcvv 3480 ∅c0 4333 𝒫 cpw 4600 {csn 4626 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pow 5365 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-dif 3954 df-ss 3968 df-nul 4334 df-pw 4602 df-sn 4627 |
| This theorem is referenced by: pp0ex 5386 dtruALT 5388 zfpair 5421 tposexg 8265 fsetexb 8904 endisj 9098 pw2eng 9118 dfac4 10162 dfac2b 10171 axcc2lem 10476 axdc2lem 10488 axcclem 10497 axpowndlem3 10639 isstruct2 17186 cat1 18142 plusffval 18659 grpinvfval 18996 grpsubfval 19001 mulgfval 19087 0symgefmndeq 19411 staffval 20842 scaffval 20878 lpival 21334 ipffval 21666 refun0 23523 filconn 23891 alexsubALTlem2 24056 nmfval 24601 tcphex 25251 tchnmfval 25262 legval 28592 locfinref 33840 oms0 34299 bnj105 34738 ssoninhaus 36449 onint1 36450 bj-tagex 36988 bj-1uplex 37009 rrnval 37834 lsatset 38991 mnuprdlem2 44292 mnuprdlem3 44293 dvnprodlem3 45963 ioorrnopn 46320 ioorrnopnxr 46322 ismeannd 46482 |
| Copyright terms: Public domain | W3C validator |