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

Theorem 0elpw 4621
Description: Every power class contains the empty set. (Contributed by NM, 25-Oct-2007.)
Assertion
Ref Expression
0elpw

Proof of Theorem 0elpw
StepHypRef Expression
1 0ss 3814 . 2
2 0ex 4582 . . 3
32elpw 4018 . 2
41, 3mpbir 209 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1818  C_wss 3475   c0 3784  ~Pcpw 4012
This theorem is referenced by:  pwne0  4622  marypha1lem  7913  brwdom2  8020  canthwdom  8026  pwcdadom  8617  isfin1-3  8787  canthp1lem2  9052  ixxssxr  11570  incexc  13649  smupf  14128  hashbc0  14523  ramz2  14542  mreexexlem3d  15043  acsfn  15056  isdrs2  15568  fpwipodrs  15794  clsval2  19551  mretopd  19593  comppfsc  20033  alexsubALTlem2  20548  alexsubALTlem4  20550  eupath2  24980  esum0  28060  esumcst  28071  esumpcvgval  28084  prsiga  28131  oms0  28266  kur14  28660  0hf  29834  0totbnd  30269  heiborlem6  30312  istopclsd  30632  dvnprodlem3  31745  lincval0  33016  lco0  33028  linds0  33066  bj-tagss  34538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-nul 4581
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-v 3111  df-dif 3478  df-in 3482  df-ss 3489  df-nul 3785  df-pw 4014
  Copyright terms: Public domain W3C validator