Theorem 0elpw 5352

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

Syntax hints:   ∈ wcel 2099   ⊆ wss 3946  ∅c0 4322  𝒫 cpw 4597

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 2697  ax-nul 5303

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-dif 3949  df-ss 3963  df-nul 4323  df-pw 4599

This theorem is referenced by:  pwne0  5353  marypha1lem  9469  brwdom2  9609  canthwdom  9615  isfin1-3  10420  canthp1lem2  10687  ixxssxr  13384  incexc  15836  smupf  16473  hashbc0  17002  ramz2  17021  mreexexlem3d  17654  acsfn  17667  isdrs2  18326  fpwipodrs  18560  pwmndid  18921  pwmnd  18922  clsval2  23042  mretopd  23084  comppfsc  23524  alexsubALTlem2  24040  alexsubALTlem4  24042  0sno  27853  bday0s  27855  0slt1s  27856  bday0b  27857  madessno  27881  oldssno  27882  newssno  27883  lltropt  27893  made0  27894  eupth2lems  30168  esum0  33895  esumcst  33909  esumpcvgval  33924  prsiga  33977  pwldsys  34003  ldgenpisyslem1  34009  carsggect  34165  kur14  35057  0hf  36014  bj-tagss  36700  bj-0int  36821  bj-mooreset  36822  bj-ismoored0  36826  topdifinfindis  37066  0totbnd  37487  heiborlem6  37530  istopclsd  42394  ntrkbimka  43742  ntrk0kbimka  43743  clsk1indlem0  43745  ntrclscls00  43770  ntrneicls11  43794  ismnushort  44012  0pwfi  44697  dvnprodlem3  45605  pwsal  45972  salexct  45991  sge0rnn0  46025  sge00  46033  psmeasure  46128  caragen0  46163  0ome  46186  isomenndlem  46187  ovn0  46223  ovnsubadd2lem  46302  smfresal  46445  sprsymrelfvlem  47098  lincval0  47834  lco0  47846  linds0  47884