Theorem 0elpw 5273

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

Syntax hints:   ∈ wcel 2108   ⊆ wss 3883  ∅c0 4253  𝒫 cpw 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-nul 5225

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-in 3890  df-ss 3900  df-nul 4254  df-pw 4532

This theorem is referenced by:  pwne0  5274  marypha1lem  9122  brwdom2  9262  canthwdom  9268  isfin1-3  10073  canthp1lem2  10340  ixxssxr  13020  incexc  15477  smupf  16113  hashbc0  16634  ramz2  16653  mreexexlem3d  17272  acsfn  17285  isdrs2  17939  fpwipodrs  18173  pwmndid  18490  pwmnd  18491  clsval2  22109  mretopd  22151  comppfsc  22591  alexsubALTlem2  23107  alexsubALTlem4  23109  eupth2lems  28503  esum0  31917  esumcst  31931  esumpcvgval  31946  prsiga  31999  pwldsys  32025  ldgenpisyslem1  32031  carsggect  32185  kur14  33078  0sno  33947  bday0s  33949  0slt1s  33950  bday0b  33951  madessno  33971  oldssno  33972  newssno  33973  made0  33984  0hf  34406  bj-tagss  35097  bj-0int  35199  bj-mooreset  35200  bj-ismoored0  35204  topdifinfindis  35444  0totbnd  35858  heiborlem6  35901  istopclsd  40438  ntrkbimka  41537  ntrk0kbimka  41538  clsk1indlem0  41540  ntrclscls00  41565  ntrneicls11  41589  ismnushort  41808  0pwfi  42496  dvnprodlem3  43379  pwsal  43746  salexct  43763  sge0rnn0  43796  sge00  43804  psmeasure  43899  caragen0  43934  0ome  43957  isomenndlem  43958  ovn0  43994  ovnsubadd2lem  44073  smfresal  44209  sprsymrelfvlem  44830  lincval0  45644  lco0  45656  linds0  45694