Theorem 0elpw 5317

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 5261	. . 3 ⊢ ∅ ∈ V
3	2	elpw 4561	. 2 ⊢ (∅ ∈ 𝒫 𝐴 ↔ ∅ ⊆ 𝐴)
4	1, 3	mpbir 234	1 ⊢ ∅ ∈ 𝒫 𝐴

This proof depends on syntax axioms:   ∈ wcel 2145   ⊆ wss 3899  ∅c0 4279  𝒫 cpw 4557

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-nul 5260

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-dif 3902  df-ss 3916  df-nul 4280  df-pw 4559

This theorem is used by:  pwne0  5318  marypha1lem  9409  brwdom2  9551  canthwdom  9557  0hf  9898  isfin1-3  10445  canthp1lem2  10719  ixxssxr  13469  incexc  15986  smupf  16628  hashbc0  17163  ramz2  17182  mreexexlem3d  17800  acsfn  17813  isdrs2  18460  fpwipodrs  18694  pwmndid  19122  pwmnd  19123  clsval2  23348  mretopd  23390  comppfsc  23831  alexsubALTlem2  24347  alexsubALTlem4  24349  0no  28177  bday0  28179  0lt1s  28180  bday0b  28181  rightge0  28189  madessno  28208  oldssno  28209  newssno  28210  lltr  28230  made0  28231  eupth2lems  30821  esplyfval0  34178  vieta  34194  esum0  34663  esumcst  34677  esumpcvgval  34692  prsiga  34745  pwldsys  34772  ldgenpisyslem1  34778  carsggect  34933  kur14  35950  mh-infprim2bi  37305  bj-tagss  37863  bj-0int  37990  bj-mooreset  37991  bj-ismoored0  37995  topdifinfindis  38237  0totbnd  38675  heiborlem6  38718  istopclsd  43664  ntrkbimka  44997  ntrk0kbimka  44998  clsk1indlem0  45000  ntrclscls00  45025  ntrneicls11  45049  ismnushort  45244  0pwfi  46019  dvnprodlem3  46902  pwsal  47269  salexct  47288  sge0rnn0  47322  sge00  47330  psmeasure  47425  caragen0  47460  0ome  47483  isomenndlem  47484  ovn0  47520  ovnsubadd2lem  47599  smfresal  47742  sprsymrelfvlem  48516  lincval0  49471  lco0  49483  linds0  49521