Theorem 0elpw 5294

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

Syntax hints:   ∈ wcel 2111   ⊆ wss 3902  ∅c0 4283  𝒫 cpw 4550

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-nul 5244

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3905  df-ss 3919  df-nul 4284  df-pw 4552

This theorem is referenced by:  pwne0  5295  marypha1lem  9317  brwdom2  9459  canthwdom  9465  isfin1-3  10274  canthp1lem2  10541  ixxssxr  13254  incexc  15741  smupf  16386  hashbc0  16914  ramz2  16933  mreexexlem3d  17549  acsfn  17562  isdrs2  18209  fpwipodrs  18443  pwmndid  18841  pwmnd  18842  clsval2  22963  mretopd  23005  comppfsc  23445  alexsubALTlem2  23961  alexsubALTlem4  23963  0sno  27768  bday0s  27770  0slt1s  27771  bday0b  27772  rightpos  27780  madessno  27799  oldssno  27800  newssno  27801  lltropt  27815  made0  27816  eupth2lems  30213  esum0  34057  esumcst  34071  esumpcvgval  34086  prsiga  34139  pwldsys  34165  ldgenpisyslem1  34171  carsggect  34326  kur14  35248  0hf  36210  bj-tagss  37013  bj-0int  37134  bj-mooreset  37135  bj-ismoored0  37139  topdifinfindis  37379  0totbnd  37812  heiborlem6  37855  istopclsd  42732  ntrkbimka  44070  ntrk0kbimka  44071  clsk1indlem0  44073  ntrclscls00  44098  ntrneicls11  44122  ismnushort  44333  0pwfi  45095  dvnprodlem3  45985  pwsal  46352  salexct  46371  sge0rnn0  46405  sge00  46413  psmeasure  46508  caragen0  46543  0ome  46566  isomenndlem  46567  ovn0  46603  ovnsubadd2lem  46682  smfresal  46825  sprsymrelfvlem  47520  lincval0  48446  lco0  48458  linds0  48496