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

Theorem 0elpw 4606
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 3813 . 2  |-  (/)  C_  A
2 0ex 4569 . . 3  |-  (/)  e.  _V
32elpw 4005 . 2  |-  ( (/)  e.  ~P A  <->  (/)  C_  A
)
41, 3mpbir 209 1  |-  (/)  e.  ~P A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1823    C_ wss 3461   (/)c0 3783   ~Pcpw 3999
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-nul 4568
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-v 3108  df-dif 3464  df-in 3468  df-ss 3475  df-nul 3784  df-pw 4001
This theorem is referenced by:  pwne0  4607  marypha1lem  7885  brwdom2  7991  canthwdom  7997  pwcdadom  8587  isfin1-3  8757  canthp1lem2  9020  ixxssxr  11544  incexc  13734  smupf  14215  hashbc0  14610  ramz2  14629  mreexexlem3d  15138  acsfn  15151  isdrs2  15770  fpwipodrs  15996  clsval2  19721  mretopd  19763  comppfsc  20202  alexsubALTlem2  20717  alexsubALTlem4  20719  eupath2  25185  esum0  28281  esumcst  28295  esumpcvgval  28310  prsiga  28364  carsggect  28529  kur14  28927  0hf  30065  0totbnd  30512  heiborlem6  30555  istopclsd  30875  dvnprodlem3  31987  lincval0  33289  lco0  33301  linds0  33339  bj-tagss  34958
  Copyright terms: Public domain W3C validator