Theorem 0elpw 5311

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 4353	. 2 ⊢ ∅ ⊆ 𝐴
2		0ex 5256	. . 3 ⊢ ∅ ∈ V
3	2	elpw 4558	. 2 ⊢ (∅ ∈ 𝒫 𝐴 ↔ ∅ ⊆ 𝐴)
4	1, 3	mpbir 233	1 ⊢ ∅ ∈ 𝒫 𝐴

Syntax hints:   ∈ wcel 2141   ⊆ wss 3904  ∅c0 4285  𝒫 cpw 4554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-nul 5255

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-dif 3907  df-ss 3921  df-nul 4286  df-pw 4556

This theorem is referenced by:  pwne0  5312  marypha1lem  9376  brwdom2  9518  canthwdom  9524  isfin1-3  10340  canthp1lem2  10608  ixxssxr  13358  incexc  15850  smupf  16495  hashbc0  17024  ramz2  17043  mreexexlem3d  17661  acsfn  17674  isdrs2  18321  fpwipodrs  18555  pwmndid  18956  pwmnd  18957  clsval2  23090  mretopd  23132  comppfsc  23572  alexsubALTlem2  24088  alexsubALTlem4  24090  0no  27879  bday0  27881  0lt1s  27882  bday0b  27883  rightge0  27891  madessno  27910  oldssno  27911  newssno  27912  lltr  27932  made0  27933  eupth2lems  30386  esplyfval0  33822  vieta  33838  esum0  34307  esumcst  34321  esumpcvgval  34336  prsiga  34389  pwldsys  34415  ldgenpisyslem1  34421  carsggect  34576  kur14  35530  0hf  36491  mh-infprim2bi  36871  bj-tagss  37429  bj-0int  37555  bj-mooreset  37556  bj-ismoored0  37560  topdifinfindis  37804  0totbnd  38236  heiborlem6  38279  istopclsd  43245  ntrkbimka  44578  ntrk0kbimka  44579  clsk1indlem0  44581  ntrclscls00  44606  ntrneicls11  44630  ismnushort  44841  0pwfi  45603  dvnprodlem3  46486  pwsal  46853  salexct  46872  sge0rnn0  46906  sge00  46914  psmeasure  47009  caragen0  47044  0ome  47067  isomenndlem  47068  ovn0  47104  ovnsubadd2lem  47183  smfresal  47326  sprsymrelfvlem  48060  lincval0  49001  lco0  49013  linds0  49051