Theorem 0elpw 5293

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

Syntax hints:   ∈ wcel 2114   ⊆ wss 3890  ∅c0 4274  𝒫 cpw 4542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-dif 3893  df-ss 3907  df-nul 4275  df-pw 4544

This theorem is referenced by:  pwne0  5294  marypha1lem  9339  brwdom2  9481  canthwdom  9487  isfin1-3  10299  canthp1lem2  10567  ixxssxr  13301  incexc  15793  smupf  16438  hashbc0  16967  ramz2  16986  mreexexlem3d  17603  acsfn  17616  isdrs2  18263  fpwipodrs  18497  pwmndid  18898  pwmnd  18899  clsval2  23025  mretopd  23067  comppfsc  23507  alexsubALTlem2  24023  alexsubALTlem4  24025  0no  27815  bday0  27817  0lt1s  27818  bday0b  27819  rightge0  27827  madessno  27846  oldssno  27847  newssno  27848  lltr  27868  made0  27869  eupth2lems  30323  esplyfval0  33723  vieta  33739  esum0  34209  esumcst  34223  esumpcvgval  34238  prsiga  34291  pwldsys  34317  ldgenpisyslem1  34323  carsggect  34478  kur14  35414  0hf  36375  mh-infprim2bi  36745  bj-tagss  37303  bj-0int  37429  bj-mooreset  37430  bj-ismoored0  37434  topdifinfindis  37676  0totbnd  38108  heiborlem6  38151  istopclsd  43146  ntrkbimka  44483  ntrk0kbimka  44484  clsk1indlem0  44486  ntrclscls00  44511  ntrneicls11  44535  ismnushort  44746  0pwfi  45508  dvnprodlem3  46394  pwsal  46761  salexct  46780  sge0rnn0  46814  sge00  46822  psmeasure  46917  caragen0  46952  0ome  46975  isomenndlem  46976  ovn0  47012  ovnsubadd2lem  47091  smfresal  47234  sprsymrelfvlem  47962  lincval0  48903  lco0  48915  linds0  48953