Theorem 0elpw 5374

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

Syntax hints:   ∈ wcel 2108   ⊆ wss 3976  ∅c0 4352  𝒫 cpw 4622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-nul 5324

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979  df-ss 3993  df-nul 4353  df-pw 4624

This theorem is referenced by:  pwne0  5375  marypha1lem  9502  brwdom2  9642  canthwdom  9648  isfin1-3  10455  canthp1lem2  10722  ixxssxr  13419  incexc  15885  smupf  16524  hashbc0  17052  ramz2  17071  mreexexlem3d  17704  acsfn  17717  isdrs2  18376  fpwipodrs  18610  pwmndid  18971  pwmnd  18972  clsval2  23079  mretopd  23121  comppfsc  23561  alexsubALTlem2  24077  alexsubALTlem4  24079  0sno  27889  bday0s  27891  0slt1s  27892  bday0b  27893  madessno  27917  oldssno  27918  newssno  27919  lltropt  27929  made0  27930  nohalf  28425  eupth2lems  30270  esum0  34013  esumcst  34027  esumpcvgval  34042  prsiga  34095  pwldsys  34121  ldgenpisyslem1  34127  carsggect  34283  kur14  35184  0hf  36141  bj-tagss  36946  bj-0int  37067  bj-mooreset  37068  bj-ismoored0  37072  topdifinfindis  37312  0totbnd  37733  heiborlem6  37776  istopclsd  42656  ntrkbimka  44000  ntrk0kbimka  44001  clsk1indlem0  44003  ntrclscls00  44028  ntrneicls11  44052  ismnushort  44270  0pwfi  44961  dvnprodlem3  45869  pwsal  46236  salexct  46255  sge0rnn0  46289  sge00  46297  psmeasure  46392  caragen0  46427  0ome  46450  isomenndlem  46451  ovn0  46487  ovnsubadd2lem  46566  smfresal  46709  sprsymrelfvlem  47364  lincval0  48144  lco0  48156  linds0  48194