Theorem 0elpw 5350

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

Syntax hints:   ∈ wcel 2099   ⊆ wss 3944  ∅c0 4318  𝒫 cpw 4598

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698  ax-nul 5300

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3471  df-dif 3947  df-in 3951  df-ss 3961  df-nul 4319  df-pw 4600

This theorem is referenced by:  pwne0  5351  marypha1lem  9448  brwdom2  9588  canthwdom  9594  isfin1-3  10401  canthp1lem2  10668  ixxssxr  13360  incexc  15807  smupf  16444  hashbc0  16965  ramz2  16984  mreexexlem3d  17617  acsfn  17630  isdrs2  18289  fpwipodrs  18523  pwmndid  18879  pwmnd  18880  clsval2  22941  mretopd  22983  comppfsc  23423  alexsubALTlem2  23939  alexsubALTlem4  23941  0sno  27746  bday0s  27748  0slt1s  27749  bday0b  27750  madessno  27774  oldssno  27775  newssno  27776  lltropt  27786  made0  27787  eupth2lems  30035  esum0  33604  esumcst  33618  esumpcvgval  33633  prsiga  33686  pwldsys  33712  ldgenpisyslem1  33718  carsggect  33874  kur14  34762  0hf  35709  bj-tagss  36395  bj-0int  36516  bj-mooreset  36517  bj-ismoored0  36521  topdifinfindis  36761  0totbnd  37181  heiborlem6  37224  istopclsd  42042  ntrkbimka  43391  ntrk0kbimka  43392  clsk1indlem0  43394  ntrclscls00  43419  ntrneicls11  43443  ismnushort  43661  0pwfi  44346  dvnprodlem3  45259  pwsal  45626  salexct  45645  sge0rnn0  45679  sge00  45687  psmeasure  45782  caragen0  45817  0ome  45840  isomenndlem  45841  ovn0  45877  ovnsubadd2lem  45956  smfresal  46099  sprsymrelfvlem  46753  lincval0  47406  lco0  47418  linds0  47456