Theorem 0elpw 5303

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

Syntax hints:   ∈ wcel 2114   ⊆ wss 3903  ∅c0 4287  𝒫 cpw 4556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5253

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-dif 3906  df-ss 3920  df-nul 4288  df-pw 4558

This theorem is referenced by:  pwne0  5304  marypha1lem  9348  brwdom2  9490  canthwdom  9496  isfin1-3  10308  canthp1lem2  10576  ixxssxr  13285  incexc  15772  smupf  16417  hashbc0  16945  ramz2  16964  mreexexlem3d  17581  acsfn  17594  isdrs2  18241  fpwipodrs  18475  pwmndid  18873  pwmnd  18874  clsval2  23006  mretopd  23048  comppfsc  23488  alexsubALTlem2  24004  alexsubALTlem4  24006  0no  27817  bday0  27819  0lt1s  27820  bday0b  27821  rightge0  27829  madessno  27848  oldssno  27849  newssno  27850  lltr  27870  made0  27871  eupth2lems  30325  esplyfval0  33740  vieta  33756  esum0  34226  esumcst  34240  esumpcvgval  34255  prsiga  34308  pwldsys  34334  ldgenpisyslem1  34340  carsggect  34495  kur14  35429  0hf  36390  bj-tagss  37222  bj-0int  37348  bj-mooreset  37349  bj-ismoored0  37353  topdifinfindis  37595  0totbnd  38018  heiborlem6  38061  istopclsd  43051  ntrkbimka  44388  ntrk0kbimka  44389  clsk1indlem0  44391  ntrclscls00  44416  ntrneicls11  44440  ismnushort  44651  0pwfi  45413  dvnprodlem3  46300  pwsal  46667  salexct  46686  sge0rnn0  46720  sge00  46728  psmeasure  46823  caragen0  46858  0ome  46881  isomenndlem  46882  ovn0  46918  ovnsubadd2lem  46997  smfresal  47140  sprsymrelfvlem  47844  lincval0  48769  lco0  48781  linds0  48819