Theorem 0elpw 5301

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

Syntax hints:   ∈ wcel 2113   ⊆ wss 3901  ∅c0 4285  𝒫 cpw 4554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-nul 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904  df-ss 3918  df-nul 4286  df-pw 4556

This theorem is referenced by:  pwne0  5302  marypha1lem  9336  brwdom2  9478  canthwdom  9484  isfin1-3  10296  canthp1lem2  10564  ixxssxr  13273  incexc  15760  smupf  16405  hashbc0  16933  ramz2  16952  mreexexlem3d  17569  acsfn  17582  isdrs2  18229  fpwipodrs  18463  pwmndid  18861  pwmnd  18862  clsval2  22994  mretopd  23036  comppfsc  23476  alexsubALTlem2  23992  alexsubALTlem4  23994  0no  27805  bday0  27807  0lt1s  27808  bday0b  27809  rightge0  27817  madessno  27836  oldssno  27837  newssno  27838  lltr  27858  made0  27859  eupth2lems  30313  esplyfval0  33722  vieta  33736  esum0  34206  esumcst  34220  esumpcvgval  34235  prsiga  34288  pwldsys  34314  ldgenpisyslem1  34320  carsggect  34475  kur14  35410  0hf  36371  bj-tagss  37181  bj-0int  37306  bj-mooreset  37307  bj-ismoored0  37311  topdifinfindis  37551  0totbnd  37974  heiborlem6  38017  istopclsd  42942  ntrkbimka  44279  ntrk0kbimka  44280  clsk1indlem0  44282  ntrclscls00  44307  ntrneicls11  44331  ismnushort  44542  0pwfi  45304  dvnprodlem3  46192  pwsal  46559  salexct  46578  sge0rnn0  46612  sge00  46620  psmeasure  46715  caragen0  46750  0ome  46773  isomenndlem  46774  ovn0  46810  ovnsubadd2lem  46889  smfresal  47032  sprsymrelfvlem  47736  lincval0  48661  lco0  48673  linds0  48711