Theorem 0elpw 5317

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

Syntax hints:   ∈ wcel 2145   ⊆ wss 3907  ∅c0 4288  𝒫 cpw 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-nul 5261

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-dif 3910  df-ss 3924  df-nul 4289  df-pw 4560

This theorem is referenced by:  pwne0  5318  marypha1lem  9381  brwdom2  9523  canthwdom  9529  isfin1-3  10358  canthp1lem2  10626  ixxssxr  13375  incexc  15881  smupf  16526  hashbc0  17055  ramz2  17074  mreexexlem3d  17692  acsfn  17705  isdrs2  18352  fpwipodrs  18586  pwmndid  18988  pwmnd  18989  clsval2  23168  mretopd  23210  comppfsc  23650  alexsubALTlem2  24166  alexsubALTlem4  24168  0no  27960  bday0  27962  0lt1s  27963  bday0b  27964  rightge0  27972  madessno  27991  oldssno  27992  newssno  27993  lltr  28013  made0  28014  eupth2lems  30498  esplyfval0  33871  vieta  33887  esum0  34356  esumcst  34370  esumpcvgval  34385  prsiga  34438  pwldsys  34464  ldgenpisyslem1  34470  carsggect  34625  kur14  35579  0hf  36540  mh-infprim2bi  36920  bj-tagss  37477  bj-0int  37603  bj-mooreset  37604  bj-ismoored0  37608  topdifinfindis  37852  0totbnd  38284  heiborlem6  38327  istopclsd  43293  ntrkbimka  44626  ntrk0kbimka  44627  clsk1indlem0  44629  ntrclscls00  44654  ntrneicls11  44678  ismnushort  44875  0pwfi  45637  dvnprodlem3  46520  pwsal  46887  salexct  46906  sge0rnn0  46940  sge00  46948  psmeasure  47043  caragen0  47078  0ome  47101  isomenndlem  47102  ovn0  47138  ovnsubadd2lem  47217  smfresal  47360  sprsymrelfvlem  48094  lincval0  49046  lco0  49058  linds0  49096