Theorem 0elpw 5355

Description: Every power class contains the empty set. (Contributed by NM, 25-Oct-2007.)

Assertion

Ref	Expression
0elpw	⊢ ∅ ∈ 𝒫 𝐴

Proof of Theorem 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 ⊢ ∅ ∈ 𝒫 𝐴

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