MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  0elpw Structured version   Unicode version

Theorem 0elpw 4459
Description: Every power class contains the empty set. (Contributed by NM, 25-Oct-2007.)
Assertion
Ref Expression
0elpw  |-  (/)  e.  ~P A

Proof of Theorem 0elpw
StepHypRef Expression
1 0ss 3664 . 2  |-  (/)  C_  A
2 0ex 4420 . . 3  |-  (/)  e.  _V
32elpw 3864 . 2  |-  ( (/)  e.  ~P A  <->  (/)  C_  A
)
41, 3mpbir 209 1  |-  (/)  e.  ~P A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756    C_ wss 3326   (/)c0 3635   ~Pcpw 3858
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422  ax-nul 4419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-v 2972  df-dif 3329  df-in 3333  df-ss 3340  df-nul 3636  df-pw 3860
This theorem is referenced by:  pwne0  4460  marypha1lem  7681  brwdom2  7786  canthwdom  7792  pwcdadom  8383  isfin1-3  8553  canthp1lem2  8818  ixxssxr  11310  incexc  13298  smupf  13672  hashbc0  14064  ramz2  14083  mreexexlem3d  14582  acsfn  14595  isdrs2  15107  fpwipodrs  15332  clsval2  18652  mretopd  18694  alexsubALTlem2  19618  alexsubALTlem4  19620  eupath2  23599  esum0  26501  esumcst  26512  esumpcvgval  26525  prsiga  26572  kur14  27102  0hf  28213  comppfsc  28576  0totbnd  28669  heiborlem6  28712  istopclsd  29033  lincval0  30946  lco0  30958  linds0  30996  bj-tagss  32470
  Copyright terms: Public domain W3C validator