Theorem 0elpw 5291

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

Syntax hints:   ∈ wcel 2105   ⊆ wss 3896  ∅c0 4266  𝒫 cpw 4543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708  ax-nul 5243

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3443  df-dif 3899  df-in 3903  df-ss 3913  df-nul 4267  df-pw 4545

This theorem is referenced by:  pwne0  5292  marypha1lem  9260  brwdom2  9400  canthwdom  9406  isfin1-3  10212  canthp1lem2  10479  ixxssxr  13161  incexc  15618  smupf  16254  hashbc0  16773  ramz2  16792  mreexexlem3d  17422  acsfn  17435  isdrs2  18091  fpwipodrs  18325  pwmndid  18642  pwmnd  18643  clsval2  22272  mretopd  22314  comppfsc  22754  alexsubALTlem2  23270  alexsubALTlem4  23272  eupth2lems  28710  esum0  32123  esumcst  32137  esumpcvgval  32152  prsiga  32205  pwldsys  32231  ldgenpisyslem1  32237  carsggect  32391  kur14  33284  0sno  34081  bday0s  34083  0slt1s  34084  bday0b  34085  madessno  34105  oldssno  34106  newssno  34107  made0  34118  0hf  34540  bj-tagss  35230  bj-0int  35332  bj-mooreset  35333  bj-ismoored0  35337  topdifinfindis  35577  0totbnd  35991  heiborlem6  36034  istopclsd  40732  ntrkbimka  41876  ntrk0kbimka  41877  clsk1indlem0  41879  ntrclscls00  41904  ntrneicls11  41928  ismnushort  42147  0pwfi  42835  dvnprodlem3  43733  pwsal  44100  salexct  44117  sge0rnn0  44151  sge00  44159  psmeasure  44254  caragen0  44289  0ome  44312  isomenndlem  44313  ovn0  44349  ovnsubadd2lem  44428  smfresal  44571  sprsymrelfvlem  45201  lincval0  46015  lco0  46027  linds0  46065