Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 0elpw | Structured version Visualization version Unicode version |
Description: Every power class contains the empty set. (Contributed by NM, 25-Oct-2007.) |
Ref | Expression |
---|---|
0elpw |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0ss 3972 | . 2 | |
2 | 0ex 4790 | . . 3 | |
3 | 2 | elpw 4164 | . 2 |
4 | 1, 3 | mpbir 221 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wcel 1990 wss 3574 c0 3915 cpw 4158 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-nul 4789 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-dif 3577 df-in 3581 df-ss 3588 df-nul 3916 df-pw 4160 |
This theorem is referenced by: pwne0 4835 marypha1lem 8339 brwdom2 8478 canthwdom 8484 pwcdadom 9038 isfin1-3 9208 canthp1lem2 9475 ixxssxr 12187 incexc 14569 smupf 15200 hashbc0 15709 ramz2 15728 mreexexlem3d 16306 acsfn 16320 isdrs2 16939 fpwipodrs 17164 clsval2 20854 mretopd 20896 comppfsc 21335 alexsubALTlem2 21852 alexsubALTlem4 21854 eupth2lems 27098 esum0 30111 esumcst 30125 esumpcvgval 30140 prsiga 30194 pwldsys 30220 ldgenpisyslem1 30226 carsggect 30380 kur14 31198 0hf 32284 bj-tagss 32968 bj-0int 33055 bj-mooreset 33056 bj-ismoored0 33061 topdifinfindis 33194 0totbnd 33572 heiborlem6 33615 istopclsd 37263 ntrkbimka 38336 ntrk0kbimka 38337 clsk1indlem0 38339 ntrclscls00 38364 ntrneicls11 38388 0pwfi 39227 dvnprodlem3 40163 pwsal 40535 salexct 40552 sge0rnn0 40585 sge00 40593 psmeasure 40688 caragen0 40720 0ome 40743 isomenndlem 40744 ovn0 40780 ovnsubadd2lem 40859 smfresal 40995 sprsymrelfvlem 41740 lincval0 42204 lco0 42216 linds0 42254 |
Copyright terms: Public domain | W3C validator |