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

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

Proof of Theorem c0ex
StepHypRef Expression
1 0cn 9374 . 2  |-  0  e.  CC
21elexi 2980 1  |-  0  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1761   _Vcvv 2970   CCcc 9276   0cc0 9278
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-12 1797  ax-ext 2422  ax-1cn 9336  ax-icn 9337  ax-addcl 9338  ax-mulcl 9340  ax-i2m1 9346
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-v 2972
This theorem is referenced by:  ofsubeq0  10315  ofsubge0  10317  elnn0  10577  un0mulcl  10610  frnnn0supp  10629  frnnn0fsupp  10631  nn0ssz  10663  nn0ind-raph  10738  xaddval  11189  xmulval  11191  ser0f  11855  facnn  12049  fac0  12050  bcval  12076  snopiswrd  12239  wrdexb  12241  repsw1  12417  cshw1  12452  s1co  12457  wrdlen2i  12542  wrd2pr2op  12543  sgnval  12573  iserge0  13134  sum0  13194  sumz  13195  fsumss  13198  fsumser  13203  isumless  13304  geomulcvg  13332  rpnnen2lem1  13493  ruclem4  13512  ruclem8  13515  0bits  13631  gcdval  13688  prmreclem2  13974  prmreclem5  13977  vdwapun  14031  odval  16030  odf  16033  gexval  16070  srgbinom  16633  abvtrivd  16905  snifpsrbag  17411  psrbaglesupp  17413  psrbagaddcl  17416  psrbaglefi  17419  mplcoe2  17525  mplbas2  17527  ltbwe  17530  psrbag0  17552  psrbagev1  17570  prdsdsf  19901  prdsxmetlem  19902  prdsmet  19904  imasdsf1olem  19907  prdsbl  20025  xrge0gsumle  20369  xrge0tsms  20370  xrhmeo  20477  pcopt  20553  pcopt2  20554  pcoass  20555  rrxcph  20855  ovoliunnul  20949  ovolicc1  20958  vitalilem5  21051  mbfpos  21088  0pval  21108  0pledm  21110  i1f1lem  21126  i1f1  21127  itg11  21128  itg1addlem3  21135  itg1addlem4  21136  i1fres  21142  itg1climres  21151  mbfi1fseqlem4  21155  mbfi1fseqlem6  21157  mbfi1flimlem  21159  mbfi1flim  21160  xrge0f  21168  itg2ge0  21172  itg2uba  21180  itg2splitlem  21185  itg2monolem1  21187  itg2gt0  21197  itg2cnlem1  21198  ibl0  21223  i1fibl  21244  itgeqa  21250  itgcn  21279  dvcmul  21377  dvcmulf  21378  dvexp3  21409  rolle  21421  dveq0  21431  dv11cn  21432  tdeglem4  21488  elply2  21623  elplyd  21629  ply1term  21631  ply0  21635  plyeq0  21638  plypf1  21639  plymullem  21643  dgrlt  21692  plymul0or  21706  dvply1  21709  plydivlem4  21721  elqaalem2  21745  aareccl  21751  aannenlem2  21754  tayl0  21786  taylpfval  21789  dvtaylp  21794  pserdvlem2  21852  abelthlem9  21864  logtayl  22064  leibpilem2  22295  leibpi  22296  jensenlem2  22340  jensen  22341  amgmlem  22342  amgm  22343  vmaval  22410  vmaf  22416  muval  22429  dchrelbas2  22535  dchrinvcl  22551  dchrptlem2  22563  lgseisenlem4  22650  pntrlog2bndlem4  22788  pntrlog2bndlem5  22789  padicval  22825  padicabv  22838  ostth1  22841  axlowdimlem8  23130  axlowdimlem9  23131  axlowdimlem10  23132  axlowdimlem11  23133  axlowdimlem12  23134  axlowdimlem13  23135  axlowdimlem17  23139  2trllemA  23384  2trllemH  23386  2trllemE  23387  2wlklemA  23388  wlkntrllem1  23393  wlkntrllem2  23394  wlkntrllem3  23395  2wlklem  23398  0spth  23405  constr1trl  23422  1pthon  23425  2pthlem2  23430  2wlklem1  23431  2pthon  23436  2pthon3v  23438  constr3lem2  23467  constr3lem4  23468  constr3lem5  23469  constr3trllem1  23471  constr3trllem2  23472  eupath  23537  occllem  24641  0cnfn  25319  0lnfn  25324  nmfn0  25326  nmcexi  25365  nlelchi  25400  sgnsval  26124  sgnsf  26125  xrge0iif1  26304  xrge0mulc1cn  26307  esumpfinval  26460  esumpfinvalf  26461  ddeval1  26586  ddeval0  26587  eulerpartlemt  26684  coinfliprv  26795  sgncl  26851  plymul02  26877  plymulx  26879  signsw0glem  26884  signsw0g  26887  signswmnd  26888  signswrid  26889  signstfvn  26900  igamval  26963  cvmliftlem4  27107  cvmliftlem5  27108  relexp0  27260  mblfinlem2  28354  mblfinlem3  28355  ismblfin  28357  itg2addnclem  28368  itg2addnclem3  28370  itg2addnc  28371  ftc1anclem3  28394  ftc1anclem5  28396  ftc1anclem7  28398  ftc1anclem8  28399  ftc1anc  28400  dvacos  28406  prdsbnd  28617  heiborlem10  28644  diophrw  29022  monotoddzzfi  29208  zindbi  29212  mncn0  29421  aaitgo  29444  flcidc  29456  ofsubid  29523  lhe4.4ex1a  29528  dvsconst  29529  dvconstbi  29533  climrec  29701  stoweidlem55  29775  wwlktovf1  30177  usgra2pthspth  30220  usgra2wlkspthlem1  30221  usgra2wlkspthlem2  30222  usgra2pthlem1  30225  usgra2pth  30226  usgra2adedglem1  30233  usg2wlkonot  30327  usg2wotspth  30328  clwwlkn2  30363  0egra0rgra  30474  rusgranumwlkl1  30484  zlmodzxzel  30669  zlmodzxz0  30670  zlmodzxzscm  30671  zlmodzxzadd  30672  zlmodzxznm  30880  zlmodzxzldeplem  30881  zlmodzxzldeplem2  30884  ex-gt  30904  ex-gte  30905  renegclALT  32336
  Copyright terms: Public domain W3C validator