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

This proof depends on syntax axioms:   ∈ wcel 2146   ⊆ wss 3908  ∅c0 4289  𝒫 cpw 4567

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-nul 5274

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-dif 3911  df-ss 3925  df-nul 4290  df-pw 4569

This theorem is used by:  pwne0  5332  marypha1lem  9403  brwdom2  9545  canthwdom  9551  isfin1-3  10388  canthp1lem2  10656  ixxssxr  13402  incexc  15917  smupf  16561  hashbc0  17090  ramz2  17109  mreexexlem3d  17727  acsfn  17740  isdrs2  18387  fpwipodrs  18621  pwmndid  19029  pwmnd  19030  clsval2  23244  mretopd  23286  comppfsc  23726  alexsubALTlem2  24242  alexsubALTlem4  24244  0no  28039  bday0  28041  0lt1s  28042  bday0b  28043  rightge0  28051  madessno  28070  oldssno  28071  newssno  28072  lltr  28092  made0  28093  eupth2lems  30626  esplyfval0  33985  vieta  34001  esum0  34470  esumcst  34484  esumpcvgval  34499  prsiga  34552  pwldsys  34579  ldgenpisyslem1  34585  carsggect  34740  kur14  35729  0hf  36690  mh-infprim2bi  37099  bj-tagss  37657  bj-0int  37784  bj-mooreset  37785  bj-ismoored0  37789  topdifinfindis  38033  0totbnd  38465  heiborlem6  38508  istopclsd  43472  ntrkbimka  44805  ntrk0kbimka  44806  clsk1indlem0  44808  ntrclscls00  44833  ntrneicls11  44857  ismnushort  45052  0pwfi  45820  dvnprodlem3  46703  pwsal  47070  salexct  47089  sge0rnn0  47123  sge00  47131  psmeasure  47226  caragen0  47261  0ome  47284  isomenndlem  47285  ovn0  47321  ovnsubadd2lem  47400  smfresal  47543  sprsymrelfvlem  48280  lincval0  49236  lco0  49248  linds0  49286