Theorem 0elpw 5328

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

Syntax hints:   ∈ wcel 2143   ⊆ wss 3906  ∅c0 4287  𝒫 cpw 4563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-nul 5270

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3909  df-ss 3923  df-nul 4288  df-pw 4565

This theorem is referenced by:  pwne0  5329  marypha1lem  9394  brwdom2  9536  canthwdom  9542  isfin1-3  10371  canthp1lem2  10639  ixxssxr  13385  incexc  15893  smupf  16537  hashbc0  17066  ramz2  17085  mreexexlem3d  17703  acsfn  17716  isdrs2  18363  fpwipodrs  18597  pwmndid  18999  pwmnd  19000  clsval2  23188  mretopd  23230  comppfsc  23670  alexsubALTlem2  24186  alexsubALTlem4  24188  0no  27980  bday0  27982  0lt1s  27983  bday0b  27984  rightge0  27992  madessno  28011  oldssno  28012  newssno  28013  lltr  28033  made0  28034  eupth2lems  30567  esplyfval0  33932  vieta  33948  esum0  34417  esumcst  34431  esumpcvgval  34446  prsiga  34499  pwldsys  34525  ldgenpisyslem1  34531  carsggect  34686  kur14  35686  0hf  36647  mh-infprim2bi  37036  bj-tagss  37594  bj-0int  37721  bj-mooreset  37722  bj-ismoored0  37726  topdifinfindis  37970  0totbnd  38402  heiborlem6  38445  istopclsd  43411  ntrkbimka  44744  ntrk0kbimka  44745  clsk1indlem0  44747  ntrclscls00  44772  ntrneicls11  44796  ismnushort  44991  0pwfi  45759  dvnprodlem3  46642  pwsal  47009  salexct  47028  sge0rnn0  47062  sge00  47070  psmeasure  47165  caragen0  47200  0ome  47223  isomenndlem  47224  ovn0  47260  ovnsubadd2lem  47339  smfresal  47482  sprsymrelfvlem  48216  lincval0  49172  lco0  49184  linds0  49222