Theorem 0elpw 5344

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

Syntax hints:   ∈ wcel 2098   ⊆ wss 3940  ∅c0 4314  𝒫 cpw 4594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695  ax-nul 5296

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468  df-dif 3943  df-in 3947  df-ss 3957  df-nul 4315  df-pw 4596

This theorem is referenced by:  pwne0  5345  marypha1lem  9424  brwdom2  9564  canthwdom  9570  isfin1-3  10377  canthp1lem2  10644  ixxssxr  13333  incexc  15780  smupf  16416  hashbc0  16937  ramz2  16956  mreexexlem3d  17589  acsfn  17602  isdrs2  18261  fpwipodrs  18495  pwmndid  18851  pwmnd  18852  clsval2  22876  mretopd  22918  comppfsc  23358  alexsubALTlem2  23874  alexsubALTlem4  23876  0sno  27675  bday0s  27677  0slt1s  27678  bday0b  27679  madessno  27703  oldssno  27704  newssno  27705  lltropt  27715  made0  27716  eupth2lems  29960  esum0  33536  esumcst  33550  esumpcvgval  33565  prsiga  33618  pwldsys  33644  ldgenpisyslem1  33650  carsggect  33806  kur14  34696  0hf  35644  bj-tagss  36351  bj-0int  36472  bj-mooreset  36473  bj-ismoored0  36477  topdifinfindis  36717  0totbnd  37131  heiborlem6  37174  istopclsd  41927  ntrkbimka  43278  ntrk0kbimka  43279  clsk1indlem0  43281  ntrclscls00  43306  ntrneicls11  43330  ismnushort  43549  0pwfi  44234  dvnprodlem3  45149  pwsal  45516  salexct  45535  sge0rnn0  45569  sge00  45577  psmeasure  45672  caragen0  45707  0ome  45730  isomenndlem  45731  ovn0  45767  ovnsubadd2lem  45846  smfresal  45989  sprsymrelfvlem  46643  lincval0  47284  lco0  47296  linds0  47334