Theorem 0elpw 5321

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

This proof depends on syntax axioms:   ∈ wcel 2147   ⊆ wss 3900  ∅c0 4281  𝒫 cpw 4560

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5263

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-dif 4050  df-nul 4282  df-pw 4562

This theorem is used by:  pwne0  5322  marypha1lem  9452  brwdom2  9594  canthwdom  9600  0hf  9944  isfin1-3  10491  canthp1lem2  10765  ixxssxr  13515  incexc  16035  smupf  16677  hashbc0  17212  ramz2  17231  mreexexlem3d  17849  acsfn  17862  isdrs2  18509  fpwipodrs  18743  pwmndid  19171  pwmnd  19172  clsval2  23398  mretopd  23440  comppfsc  23881  alexsubALTlem2  24397  alexsubALTlem4  24399  0no  28225  bday0  28227  0lt1s  28228  bday0b  28229  rightge0  28237  madessno  28256  oldssno  28257  newssno  28258  lltr  28278  made0  28279  eupth2lems  30869  esplyfval0  34266  vieta  34282  esum0  34751  esumcst  34765  esumpcvgval  34780  prsiga  34833  pwldsys  34860  ldgenpisyslem1  34866  carsggect  35020  kur14  36148  mh-infprim2bi  37513  bj-tagss  38071  bj-0int  38213  bj-mooreset  38214  bj-ismoored0  38218  topdifinfindis  38461  0totbnd  38899  heiborlem6  38942  istopclsd  43904  ntrkbimka  45230  ntrk0kbimka  45231  clsk1indlem0  45233  ntrclscls00  45258  ntrneicls11  45282  ismnushort  45477  0pwfi  46281  dvnprodlem3  47163  pwsal  47530  salexct  47549  sge0rnn0  47583  sge00  47591  psmeasure  47686  caragen0  47721  0ome  47744  isomenndlem  47745  ovn0  47781  ovnsubadd2lem  47860  smfresal  48003  sprsymrelfvlem  48777  lincval0  49732  lco0  49744  linds0  49782