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

Theorem c0ex 8832
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 8831 . 2  |-  0  e.  CC
21elexi 2797 1  |-  0  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1684   _Vcvv 2788   CCcc 8735   0cc0 8737
This theorem is referenced by:  ofsubeq0  9743  ofsubge0  9745  elnn0  9967  un0mulcl  9998  nn0ssz  10044  nn0ind-raph  10112  xaddval  10550  xmulval  10552  ser0f  11099  facnn  11290  fac0  11291  bcval  11317  wrdexb  11449  s1co  11488  iserge0  12134  sum0  12194  sumz  12195  fsumss  12198  fsumser  12203  isumless  12304  geomulcvg  12332  rpnnen2lem1  12493  ruclem4  12512  ruclem8  12515  0bits  12630  gcdval  12687  prmreclem2  12964  prmreclem5  12967  vdwapun  13021  odval  14849  odf  14852  gexval  14889  abvtrivd  15605  psrbag0  16235  prdsdsf  17931  prdsxmetlem  17932  prdsmet  17934  prdsbl  18037  xrhmeo  18444  pcopt  18520  pcopt2  18521  pcoass  18522  ovoliunnul  18866  ovolicc1  18875  vitalilem5  18967  mbfpos  19006  0pval  19026  0pledm  19028  i1fd  19036  i1f1lem  19044  i1f1  19045  itg11  19046  itg1addlem3  19053  itg1addlem4  19054  i1fres  19060  itg1climres  19069  mbfi1fseqlem4  19073  mbfi1fseqlem6  19075  mbfi1flimlem  19077  mbfi1flim  19078  xrge0f  19086  itg2ge0  19090  itg2uba  19098  itg2splitlem  19103  itg2monolem1  19105  itg2gt0  19115  itg2cnlem1  19116  ibl0  19141  i1fibl  19162  itgeqa  19168  itgcn  19197  dvcmul  19293  dvcmulf  19294  dvexp3  19325  rolle  19337  dveq0  19347  dv11cn  19348  tdeglem4  19446  elply2  19578  elplyd  19584  ply1term  19586  ply0  19590  plyeq0  19593  plymullem  19598  dgrlt  19647  plymul0or  19661  dvply1  19664  plydivlem4  19676  elqaalem2  19700  aareccl  19706  aannenlem2  19709  dvtaylp  19749  pserdvlem2  19804  abelthlem9  19816  logtayl  20007  leibpilem2  20237  leibpi  20238  vmaval  20351  vmaf  20357  muval  20370  dchrelbas2  20476  dchrinvcl  20492  dchrptlem2  20504  pntrlog2bndlem4  20729  pntrlog2bndlem5  20730  padicval  20766  padicabv  20779  ostth1  20782  occllem  21882  0cnfn  22560  0lnfn  22565  nmfn0  22567  nmcexi  22606  nlelchi  22641  xrge0iif1  23320  coinfliprv  23683  cvmliftlem4  23819  cvmliftlem5  23820  eupath  23905  relexp0  24025  axlowdimlem8  24577  axlowdimlem9  24578  axlowdimlem10  24579  axlowdimlem11  24580  axlowdimlem12  24581  axlowdimlem17  24586  prdsbnd  26517  heiborlem10  26544  diophrw  26838  monotoddzzfi  27027  zindbi  27031  mncn0  27344  aaitgo  27367  flcidc  27379  ofsubid  27541  lhe4.4ex1a  27546  dvsconst  27547  dvconstbi  27551  climrec  27729  ex-gt  28198  ex-gte  28199  sgnval  28245
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-mulcl 8799  ax-i2m1 8805
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-v 2790
  Copyright terms: Public domain W3C validator