Theorem 0elpw 5279

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 4331	. 2 ⊢ ∅ ⊆ 𝐴
2		0ex 5232	. . 3 ⊢ ∅ ∈ V
3	2	elpw 4538	. 2 ⊢ (∅ ∈ 𝒫 𝐴 ↔ ∅ ⊆ 𝐴)
4	1, 3	mpbir 230	1 ⊢ ∅ ∈ 𝒫 𝐴

Syntax hints:   ∈ wcel 2107   ⊆ wss 3888  ∅c0 4257  𝒫 cpw 4534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-nul 5231

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-dif 3891  df-in 3895  df-ss 3905  df-nul 4258  df-pw 4536

This theorem is referenced by:  pwne0  5280  marypha1lem  9201  brwdom2  9341  canthwdom  9347  isfin1-3  10151  canthp1lem2  10418  ixxssxr  13100  incexc  15558  smupf  16194  hashbc0  16715  ramz2  16734  mreexexlem3d  17364  acsfn  17377  isdrs2  18033  fpwipodrs  18267  pwmndid  18584  pwmnd  18585  clsval2  22210  mretopd  22252  comppfsc  22692  alexsubALTlem2  23208  alexsubALTlem4  23210  eupth2lems  28611  esum0  32026  esumcst  32040  esumpcvgval  32055  prsiga  32108  pwldsys  32134  ldgenpisyslem1  32140  carsggect  32294  kur14  33187  0sno  34029  bday0s  34031  0slt1s  34032  bday0b  34033  madessno  34053  oldssno  34054  newssno  34055  made0  34066  0hf  34488  bj-tagss  35179  bj-0int  35281  bj-mooreset  35282  bj-ismoored0  35286  topdifinfindis  35526  0totbnd  35940  heiborlem6  35983  istopclsd  40529  ntrkbimka  41655  ntrk0kbimka  41656  clsk1indlem0  41658  ntrclscls00  41683  ntrneicls11  41707  ismnushort  41926  0pwfi  42614  dvnprodlem3  43496  pwsal  43863  salexct  43880  sge0rnn0  43913  sge00  43921  psmeasure  44016  caragen0  44051  0ome  44074  isomenndlem  44075  ovn0  44111  ovnsubadd2lem  44190  smfresal  44333  sprsymrelfvlem  44953  lincval0  45767  lco0  45779  linds0  45817