Theorem 0elpw 5362

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 4406	. 2 ⊢ ∅ ⊆ 𝐴
2		0ex 5313	. . 3 ⊢ ∅ ∈ V
3	2	elpw 4609	. 2 ⊢ (∅ ∈ 𝒫 𝐴 ↔ ∅ ⊆ 𝐴)
4	1, 3	mpbir 231	1 ⊢ ∅ ∈ 𝒫 𝐴

Syntax hints:   ∈ wcel 2106   ⊆ wss 3963  ∅c0 4339  𝒫 cpw 4605

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-nul 5312

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-dif 3966  df-ss 3980  df-nul 4340  df-pw 4607

This theorem is referenced by:  pwne0  5363  marypha1lem  9471  brwdom2  9611  canthwdom  9617  isfin1-3  10424  canthp1lem2  10691  ixxssxr  13396  incexc  15870  smupf  16512  hashbc0  17039  ramz2  17058  mreexexlem3d  17691  acsfn  17704  isdrs2  18364  fpwipodrs  18598  pwmndid  18962  pwmnd  18963  clsval2  23074  mretopd  23116  comppfsc  23556  alexsubALTlem2  24072  alexsubALTlem4  24074  0sno  27886  bday0s  27888  0slt1s  27889  bday0b  27890  madessno  27914  oldssno  27915  newssno  27916  lltropt  27926  made0  27927  nohalf  28422  eupth2lems  30267  esum0  34030  esumcst  34044  esumpcvgval  34059  prsiga  34112  pwldsys  34138  ldgenpisyslem1  34144  carsggect  34300  kur14  35201  0hf  36159  bj-tagss  36963  bj-0int  37084  bj-mooreset  37085  bj-ismoored0  37089  topdifinfindis  37329  0totbnd  37760  heiborlem6  37803  istopclsd  42688  ntrkbimka  44028  ntrk0kbimka  44029  clsk1indlem0  44031  ntrclscls00  44056  ntrneicls11  44080  ismnushort  44297  0pwfi  44999  dvnprodlem3  45904  pwsal  46271  salexct  46290  sge0rnn0  46324  sge00  46332  psmeasure  46427  caragen0  46462  0ome  46485  isomenndlem  46486  ovn0  46522  ovnsubadd2lem  46601  smfresal  46744  sprsymrelfvlem  47415  lincval0  48261  lco0  48273  linds0  48311