Theorem 0elpw 5331

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

Syntax hints:   ∈ wcel 2109   ⊆ wss 3931  ∅c0 4313  𝒫 cpw 4580

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 2708  ax-nul 5281

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 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-dif 3934  df-ss 3948  df-nul 4314  df-pw 4582

This theorem is referenced by:  pwne0  5332  marypha1lem  9450  brwdom2  9592  canthwdom  9598  isfin1-3  10405  canthp1lem2  10672  ixxssxr  13379  incexc  15858  smupf  16502  hashbc0  17030  ramz2  17049  mreexexlem3d  17663  acsfn  17676  isdrs2  18323  fpwipodrs  18555  pwmndid  18919  pwmnd  18920  clsval2  22993  mretopd  23035  comppfsc  23475  alexsubALTlem2  23991  alexsubALTlem4  23993  0sno  27795  bday0s  27797  0slt1s  27798  bday0b  27799  madessno  27825  oldssno  27826  newssno  27827  lltropt  27841  made0  27842  eupth2lems  30224  esum0  34085  esumcst  34099  esumpcvgval  34114  prsiga  34167  pwldsys  34193  ldgenpisyslem1  34199  carsggect  34355  kur14  35243  0hf  36200  bj-tagss  37003  bj-0int  37124  bj-mooreset  37125  bj-ismoored0  37129  topdifinfindis  37369  0totbnd  37802  heiborlem6  37845  istopclsd  42690  ntrkbimka  44029  ntrk0kbimka  44030  clsk1indlem0  44032  ntrclscls00  44057  ntrneicls11  44081  ismnushort  44292  0pwfi  45050  dvnprodlem3  45944  pwsal  46311  salexct  46330  sge0rnn0  46364  sge00  46372  psmeasure  46467  caragen0  46502  0ome  46525  isomenndlem  46526  ovn0  46562  ovnsubadd2lem  46641  smfresal  46784  sprsymrelfvlem  47471  lincval0  48358  lco0  48370  linds0  48408