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 4347 | . 2 ⊢ ∅ ⊆ 𝐴 | |
2 | 0ex 5202 | . . 3 ⊢ ∅ ∈ V | |
3 | 2 | elpw 4542 | . 2 ⊢ (∅ ∈ 𝒫 𝐴 ↔ ∅ ⊆ 𝐴) |
4 | 1, 3 | mpbir 232 | 1 ⊢ ∅ ∈ 𝒫 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2105 ⊆ wss 3933 ∅c0 4288 𝒫 cpw 4535 |
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-nul 5201 |
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 |
This theorem is referenced by: pwne0 5248 marypha1lem 8885 brwdom2 9025 canthwdom 9031 isfin1-3 9796 canthp1lem2 10063 ixxssxr 12738 incexc 15180 smupf 15815 hashbc0 16329 ramz2 16348 mreexexlem3d 16905 acsfn 16918 isdrs2 17537 fpwipodrs 17762 pwmndid 18039 pwmnd 18040 clsval2 21586 mretopd 21628 comppfsc 22068 alexsubALTlem2 22584 alexsubALTlem4 22586 eupth2lems 27944 esum0 31207 esumcst 31221 esumpcvgval 31236 prsiga 31289 pwldsys 31315 ldgenpisyslem1 31321 carsggect 31475 kur14 32360 0hf 33535 bj-tagss 34189 bj-0int 34287 bj-mooreset 34288 bj-ismoored0 34292 topdifinfindis 34509 0totbnd 34932 heiborlem6 34975 istopclsd 39175 ntrkbimka 40266 ntrk0kbimka 40267 clsk1indlem0 40269 ntrclscls00 40294 ntrneicls11 40318 0pwfi 41198 dvnprodlem3 42109 pwsal 42477 salexct 42494 sge0rnn0 42527 sge00 42535 psmeasure 42630 caragen0 42665 0ome 42688 isomenndlem 42689 ovn0 42725 ovnsubadd2lem 42804 smfresal 42940 sprsymrelfvlem 43529 lincval0 44398 lco0 44410 linds0 44448 |
Copyright terms: Public domain | W3C validator |