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  37302  bj-mooreset  37303  bj-ismoored0  37307  topdifinfindis  37547  0totbnd  37970  heiborlem6  38013  istopclsd  42938  ntrkbimka  44275  ntrk0kbimka  44276  clsk1indlem0  44278  ntrclscls00  44303  ntrneicls11  44327  ismnushort  44538  0pwfi  45300  dvnprodlem3  46188  pwsal  46555  salexct  46574  sge0rnn0  46608  sge00  46616  psmeasure  46711  caragen0  46746  0ome  46769  isomenndlem  46770  ovn0  46806  ovnsubadd2lem  46885  smfresal  47028  sprsymrelfvlem  47732  lincval0  48657  lco0  48669  linds0  48707