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

Theorem 0elpw 4361
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 3648 . 2  |-  (/)  C_  A
2 0ex 4331 . . 3  |-  (/)  e.  _V
32elpw 3797 . 2  |-  ( (/)  e.  ~P A  <->  (/)  C_  A
)
41, 3mpbir 201 1  |-  (/)  e.  ~P A
Colors of variables: wff set class
Syntax hints:    e. wcel 1725    C_ wss 3312   (/)c0 3620   ~Pcpw 3791
This theorem is referenced by:  marypha1lem  7430  brwdom2  7533  canthwdom  7539  pwcdadom  8088  isfin1-3  8258  canthp1lem2  8520  ixxssxr  10920  incexc  12609  smupf  12982  hashbc0  13365  ramz2  13384  mreexexlem3d  13863  acsfn  13876  isdrs2  14388  fpwipodrs  14582  clsval2  17106  mretopd  17148  alexsubALTlem2  18071  alexsubALTlem4  18073  eupath2  21694  esum0  24436  esumcst  24447  esumpcvgval  24460  prsiga  24506  kur14  24894  0hf  26110  comppfsc  26378  0totbnd  26473  heiborlem6  26516  istopclsd  26745
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-nul 4330
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-v 2950  df-dif 3315  df-in 3319  df-ss 3326  df-nul 3621  df-pw 3793
  Copyright terms: Public domain W3C validator