Theorem 0elpw 5298

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

Syntax hints:   ∈ wcel 2109   ⊆ wss 3905  ∅c0 4286  𝒫 cpw 4553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5248

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-dif 3908  df-ss 3922  df-nul 4287  df-pw 4555

This theorem is referenced by:  pwne0  5299  marypha1lem  9342  brwdom2  9484  canthwdom  9490  isfin1-3  10299  canthp1lem2  10566  ixxssxr  13278  incexc  15762  smupf  16407  hashbc0  16935  ramz2  16954  mreexexlem3d  17570  acsfn  17583  isdrs2  18230  fpwipodrs  18464  pwmndid  18828  pwmnd  18829  clsval2  22953  mretopd  22995  comppfsc  23435  alexsubALTlem2  23951  alexsubALTlem4  23953  0sno  27758  bday0s  27760  0slt1s  27761  bday0b  27762  madessno  27788  oldssno  27789  newssno  27790  lltropt  27804  made0  27805  eupth2lems  30200  esum0  34015  esumcst  34029  esumpcvgval  34044  prsiga  34097  pwldsys  34123  ldgenpisyslem1  34129  carsggect  34285  kur14  35188  0hf  36150  bj-tagss  36953  bj-0int  37074  bj-mooreset  37075  bj-ismoored0  37079  topdifinfindis  37319  0totbnd  37752  heiborlem6  37795  istopclsd  42673  ntrkbimka  44011  ntrk0kbimka  44012  clsk1indlem0  44014  ntrclscls00  44039  ntrneicls11  44063  ismnushort  44274  0pwfi  45037  dvnprodlem3  45930  pwsal  46297  salexct  46316  sge0rnn0  46350  sge00  46358  psmeasure  46453  caragen0  46488  0ome  46511  isomenndlem  46512  ovn0  46548  ovnsubadd2lem  46627  smfresal  46770  sprsymrelfvlem  47475  lincval0  48401  lco0  48413  linds0  48451