|   | 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 4399 | . 2 ⊢ ∅ ⊆ 𝐴 | |
| 2 | 0ex 5306 | . . 3 ⊢ ∅ ∈ V | |
| 3 | 2 | elpw 4603 | . 2 ⊢ (∅ ∈ 𝒫 𝐴 ↔ ∅ ⊆ 𝐴) | 
| 4 | 1, 3 | mpbir 231 | 1 ⊢ ∅ ∈ 𝒫 𝐴 | 
| Colors of variables: wff setvar class | 
| Syntax hints: ∈ wcel 2107 ⊆ wss 3950 ∅c0 4332 𝒫 cpw 4599 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 ax-nul 5305 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1542 df-fal 1552 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-v 3481 df-dif 3953 df-ss 3967 df-nul 4333 df-pw 4601 | 
| This theorem is referenced by: pwne0 5356 marypha1lem 9474 brwdom2 9614 canthwdom 9620 isfin1-3 10427 canthp1lem2 10694 ixxssxr 13400 incexc 15874 smupf 16516 hashbc0 17044 ramz2 17063 mreexexlem3d 17690 acsfn 17703 isdrs2 18353 fpwipodrs 18586 pwmndid 18950 pwmnd 18951 clsval2 23059 mretopd 23101 comppfsc 23541 alexsubALTlem2 24057 alexsubALTlem4 24059 0sno 27872 bday0s 27874 0slt1s 27875 bday0b 27876 madessno 27900 oldssno 27901 newssno 27902 lltropt 27912 made0 27913 nohalf 28408 eupth2lems 30258 esum0 34051 esumcst 34065 esumpcvgval 34080 prsiga 34133 pwldsys 34159 ldgenpisyslem1 34165 carsggect 34321 kur14 35222 0hf 36179 bj-tagss 36982 bj-0int 37103 bj-mooreset 37104 bj-ismoored0 37108 topdifinfindis 37348 0totbnd 37781 heiborlem6 37824 istopclsd 42716 ntrkbimka 44056 ntrk0kbimka 44057 clsk1indlem0 44059 ntrclscls00 44084 ntrneicls11 44108 ismnushort 44325 0pwfi 45069 dvnprodlem3 45968 pwsal 46335 salexct 46354 sge0rnn0 46388 sge00 46396 psmeasure 46491 caragen0 46526 0ome 46549 isomenndlem 46550 ovn0 46586 ovnsubadd2lem 46665 smfresal 46808 sprsymrelfvlem 47482 lincval0 48337 lco0 48349 linds0 48387 | 
| Copyright terms: Public domain | W3C validator |