Theorem 0elpw 5225

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 4293	. 2 ⊢ ∅ ⊆ 𝐴
2		0ex 5178	. . 3 ⊢ ∅ ∈ V
3	2	elpw 4499	. 2 ⊢ (∅ ∈ 𝒫 𝐴 ↔ ∅ ⊆ 𝐴)
4	1, 3	mpbir 234	1 ⊢ ∅ ∈ 𝒫 𝐴

Syntax hints:   ∈ wcel 2112   ⊆ wss 3859  ∅c0 4226  𝒫 cpw 4495

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730  ax-nul 5177

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-v 3412  df-dif 3862  df-in 3866  df-ss 3876  df-nul 4227  df-pw 4497

This theorem is referenced by:  pwne0  5226  marypha1lem  8931  brwdom2  9071  canthwdom  9077  isfin1-3  9847  canthp1lem2  10114  ixxssxr  12792  incexc  15241  smupf  15878  hashbc0  16397  ramz2  16416  mreexexlem3d  16976  acsfn  16989  isdrs2  17616  fpwipodrs  17841  pwmndid  18168  pwmnd  18169  clsval2  21751  mretopd  21793  comppfsc  22233  alexsubALTlem2  22749  alexsubALTlem4  22751  eupth2lems  28123  esum0  31537  esumcst  31551  esumpcvgval  31566  prsiga  31619  pwldsys  31645  ldgenpisyslem1  31651  carsggect  31805  kur14  32695  0sno  33581  bday0s  33583  0slt1s  33584  bday0b  33585  made0  33615  0hf  34029  bj-tagss  34698  bj-0int  34797  bj-mooreset  34798  bj-ismoored0  34802  topdifinfindis  35044  0totbnd  35492  heiborlem6  35535  istopclsd  40015  ntrkbimka  41115  ntrk0kbimka  41116  clsk1indlem0  41118  ntrclscls00  41143  ntrneicls11  41167  0pwfi  42067  dvnprodlem3  42957  pwsal  43324  salexct  43341  sge0rnn0  43374  sge00  43382  psmeasure  43477  caragen0  43512  0ome  43535  isomenndlem  43536  ovn0  43572  ovnsubadd2lem  43651  smfresal  43787  sprsymrelfvlem  44376  lincval0  45190  lco0  45202  linds0  45240