![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 0elpw | Structured version Visualization version GIF version |
Description: Every power class contains the empty set. (Contributed by NM, 25-Oct-2007.) |
Ref | Expression |
---|---|
0elpw | ⊢ ∅ ∈ 𝒫 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0ss 4394 | . 2 ⊢ ∅ ⊆ 𝐴 | |
2 | 0ex 5304 | . . 3 ⊢ ∅ ∈ V | |
3 | 2 | elpw 4601 | . 2 ⊢ (∅ ∈ 𝒫 𝐴 ↔ ∅ ⊆ 𝐴) |
4 | 1, 3 | mpbir 230 | 1 ⊢ ∅ ∈ 𝒫 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2099 ⊆ wss 3946 ∅c0 4322 𝒫 cpw 4597 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 ax-nul 5303 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-v 3464 df-dif 3949 df-ss 3963 df-nul 4323 df-pw 4599 |
This theorem is referenced by: pwne0 5353 marypha1lem 9469 brwdom2 9609 canthwdom 9615 isfin1-3 10420 canthp1lem2 10687 ixxssxr 13384 incexc 15836 smupf 16473 hashbc0 17002 ramz2 17021 mreexexlem3d 17654 acsfn 17667 isdrs2 18326 fpwipodrs 18560 pwmndid 18921 pwmnd 18922 clsval2 23042 mretopd 23084 comppfsc 23524 alexsubALTlem2 24040 alexsubALTlem4 24042 0sno 27853 bday0s 27855 0slt1s 27856 bday0b 27857 madessno 27881 oldssno 27882 newssno 27883 lltropt 27893 made0 27894 eupth2lems 30168 esum0 33895 esumcst 33909 esumpcvgval 33924 prsiga 33977 pwldsys 34003 ldgenpisyslem1 34009 carsggect 34165 kur14 35057 0hf 36014 bj-tagss 36700 bj-0int 36821 bj-mooreset 36822 bj-ismoored0 36826 topdifinfindis 37066 0totbnd 37487 heiborlem6 37530 istopclsd 42394 ntrkbimka 43742 ntrk0kbimka 43743 clsk1indlem0 43745 ntrclscls00 43770 ntrneicls11 43794 ismnushort 44012 0pwfi 44697 dvnprodlem3 45605 pwsal 45972 salexct 45991 sge0rnn0 46025 sge00 46033 psmeasure 46128 caragen0 46163 0ome 46186 isomenndlem 46187 ovn0 46223 ovnsubadd2lem 46302 smfresal 46445 sprsymrelfvlem 47098 lincval0 47834 lco0 47846 linds0 47884 |
Copyright terms: Public domain | W3C validator |