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

Theorem c0ex 8848
Description: 0 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.)
Assertion
Ref Expression
c0ex  |-  0  e.  _V

Proof of Theorem c0ex
StepHypRef Expression
1 0cn 8847 . 2  |-  0  e.  CC
21elexi 2810 1  |-  0  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1696   _Vcvv 2801   CCcc 8751   0cc0 8753
This theorem is referenced by:  ofsubeq0  9759  ofsubge0  9761  elnn0  9983  un0mulcl  10014  nn0ssz  10060  nn0ind-raph  10128  xaddval  10566  xmulval  10568  ser0f  11115  facnn  11306  fac0  11307  bcval  11333  wrdexb  11465  s1co  11504  iserge0  12150  sum0  12210  sumz  12211  fsumss  12214  fsumser  12219  isumless  12320  geomulcvg  12348  rpnnen2lem1  12509  ruclem4  12528  ruclem8  12531  0bits  12646  gcdval  12703  prmreclem2  12980  prmreclem5  12983  vdwapun  13037  odval  14865  odf  14868  gexval  14905  abvtrivd  15621  psrbag0  16251  prdsdsf  17947  prdsxmetlem  17948  prdsmet  17950  prdsbl  18053  xrhmeo  18460  pcopt  18536  pcopt2  18537  pcoass  18538  ovoliunnul  18882  ovolicc1  18891  vitalilem5  18983  mbfpos  19022  0pval  19042  0pledm  19044  i1fd  19052  i1f1lem  19060  i1f1  19061  itg11  19062  itg1addlem3  19069  itg1addlem4  19070  i1fres  19076  itg1climres  19085  mbfi1fseqlem4  19089  mbfi1fseqlem6  19091  mbfi1flimlem  19093  mbfi1flim  19094  xrge0f  19102  itg2ge0  19106  itg2uba  19114  itg2splitlem  19119  itg2monolem1  19121  itg2gt0  19131  itg2cnlem1  19132  ibl0  19157  i1fibl  19178  itgeqa  19184  itgcn  19213  dvcmul  19309  dvcmulf  19310  dvexp3  19341  rolle  19353  dveq0  19363  dv11cn  19364  tdeglem4  19462  elply2  19594  elplyd  19600  ply1term  19602  ply0  19606  plyeq0  19609  plymullem  19614  dgrlt  19663  plymul0or  19677  dvply1  19680  plydivlem4  19692  elqaalem2  19716  aareccl  19722  aannenlem2  19725  dvtaylp  19765  pserdvlem2  19820  abelthlem9  19832  logtayl  20023  leibpilem2  20253  leibpi  20254  vmaval  20367  vmaf  20373  muval  20386  dchrelbas2  20492  dchrinvcl  20508  dchrptlem2  20520  pntrlog2bndlem4  20745  pntrlog2bndlem5  20746  padicval  20782  padicabv  20795  ostth1  20798  occllem  21898  0cnfn  22576  0lnfn  22581  nmfn0  22583  nmcexi  22622  nlelchi  22657  xrge0iif1  23335  coinfliprv  23698  cvmliftlem4  23834  cvmliftlem5  23835  eupath  23920  relexp0  24040  axlowdimlem8  24649  axlowdimlem9  24650  axlowdimlem10  24651  axlowdimlem11  24652  axlowdimlem12  24653  axlowdimlem17  24658  itg2addnclem  25003  itg2addnc  25005  prdsbnd  26620  heiborlem10  26647  diophrw  26941  monotoddzzfi  27130  zindbi  27134  mncn0  27447  aaitgo  27470  flcidc  27482  ofsubid  27644  lhe4.4ex1a  27649  dvsconst  27650  dvconstbi  27654  climrec  27832  wlkntrllem1  28345  wlkntrllem2  28346  wlkntrllem3  28347  wlkntrllem4  28348  wlkntrllem5  28349  0spth  28357  constr3lem2  28392  constr3lem4  28393  constr3lem5  28394  constr3trllem1  28396  constr3trllem2  28397  ex-gt  28452  ex-gte  28453  sgnval  28499
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277  ax-1cn 8811  ax-icn 8812  ax-addcl 8813  ax-mulcl 8815  ax-i2m1 8821
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-v 2803
  Copyright terms: Public domain W3C validator