Theorem 0elpw 5296

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

Syntax hints:   ∈ wcel 2113   ⊆ wss 3898  ∅c0 4282  𝒫 cpw 4549

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 2705  ax-nul 5246

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 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-dif 3901  df-ss 3915  df-nul 4283  df-pw 4551

This theorem is referenced by:  pwne0  5297  marypha1lem  9324  brwdom2  9466  canthwdom  9472  isfin1-3  10284  canthp1lem2  10551  ixxssxr  13259  incexc  15746  smupf  16391  hashbc0  16919  ramz2  16938  mreexexlem3d  17554  acsfn  17567  isdrs2  18214  fpwipodrs  18448  pwmndid  18846  pwmnd  18847  clsval2  22966  mretopd  23008  comppfsc  23448  alexsubALTlem2  23964  alexsubALTlem4  23966  0sno  27771  bday0s  27773  0slt1s  27774  bday0b  27775  rightpos  27783  madessno  27802  oldssno  27803  newssno  27804  lltropt  27818  made0  27819  eupth2lems  30220  esum0  34083  esumcst  34097  esumpcvgval  34112  prsiga  34165  pwldsys  34191  ldgenpisyslem1  34197  carsggect  34352  kur14  35281  0hf  36242  bj-tagss  37045  bj-0int  37166  bj-mooreset  37167  bj-ismoored0  37171  topdifinfindis  37411  0totbnd  37833  heiborlem6  37876  istopclsd  42817  ntrkbimka  44155  ntrk0kbimka  44156  clsk1indlem0  44158  ntrclscls00  44183  ntrneicls11  44207  ismnushort  44418  0pwfi  45180  dvnprodlem3  46070  pwsal  46437  salexct  46456  sge0rnn0  46490  sge00  46498  psmeasure  46593  caragen0  46628  0ome  46651  isomenndlem  46652  ovn0  46688  ovnsubadd2lem  46767  smfresal  46910  sprsymrelfvlem  47614  lincval0  48540  lco0  48552  linds0  48590