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

Syntax hints:   ∈ wcel 2109   ⊆ wss 3914  ∅c0 4296  𝒫 cpw 4563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5261

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-dif 3917  df-ss 3931  df-nul 4297  df-pw 4565

This theorem is referenced by:  pwne0  5312  marypha1lem  9384  brwdom2  9526  canthwdom  9532  isfin1-3  10339  canthp1lem2  10606  ixxssxr  13318  incexc  15803  smupf  16448  hashbc0  16976  ramz2  16995  mreexexlem3d  17607  acsfn  17620  isdrs2  18267  fpwipodrs  18499  pwmndid  18863  pwmnd  18864  clsval2  22937  mretopd  22979  comppfsc  23419  alexsubALTlem2  23935  alexsubALTlem4  23937  0sno  27738  bday0s  27740  0slt1s  27741  bday0b  27742  madessno  27768  oldssno  27769  newssno  27770  lltropt  27784  made0  27785  eupth2lems  30167  esum0  34039  esumcst  34053  esumpcvgval  34068  prsiga  34121  pwldsys  34147  ldgenpisyslem1  34153  carsggect  34309  kur14  35203  0hf  36165  bj-tagss  36968  bj-0int  37089  bj-mooreset  37090  bj-ismoored0  37094  topdifinfindis  37334  0totbnd  37767  heiborlem6  37810  istopclsd  42688  ntrkbimka  44027  ntrk0kbimka  44028  clsk1indlem0  44030  ntrclscls00  44055  ntrneicls11  44079  ismnushort  44290  0pwfi  45053  dvnprodlem3  45946  pwsal  46313  salexct  46332  sge0rnn0  46366  sge00  46374  psmeasure  46469  caragen0  46504  0ome  46527  isomenndlem  46528  ovn0  46564  ovnsubadd2lem  46643  smfresal  46786  sprsymrelfvlem  47488  lincval0  48401  lco0  48413  linds0  48451