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

Theorem c0ex 9392
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 9390 . 2  |-  0  e.  CC
21elexi 2994 1  |-  0  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756   _Vcvv 2984   CCcc 9292   0cc0 9294
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423  ax-1cn 9352  ax-icn 9353  ax-addcl 9354  ax-mulcl 9356  ax-i2m1 9362
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-v 2986
This theorem is referenced by:  ofsubeq0  10331  ofsubge0  10333  elnn0  10593  un0mulcl  10626  frnnn0supp  10645  frnnn0fsupp  10647  nn0ssz  10679  nn0ind-raph  10754  xaddval  11205  xmulval  11207  ser0f  11871  facnn  12065  fac0  12066  bcval  12092  snopiswrd  12255  wrdexb  12257  repsw1  12433  cshw1  12468  s1co  12473  wrdlen2i  12558  wrd2pr2op  12559  sgnval  12589  iserge0  13150  sum0  13210  sumz  13211  fsumss  13214  fsumser  13219  isumless  13320  geomulcvg  13348  rpnnen2lem1  13509  ruclem4  13528  ruclem8  13531  0bits  13647  gcdval  13704  prmreclem2  13990  prmreclem5  13993  vdwapun  14047  odval  16049  odf  16052  gexval  16089  srgbinom  16655  abvtrivd  16937  snifpsrbag  17445  psrbaglesupp  17447  psrbagaddcl  17450  psrbaglefi  17453  mplcoe5  17560  mplbas2  17563  ltbwe  17566  psrbag0  17588  psrbagev1  17606  prdsdsf  19954  prdsxmetlem  19955  prdsmet  19957  imasdsf1olem  19960  prdsbl  20078  xrge0gsumle  20422  xrge0tsms  20423  xrhmeo  20530  pcopt  20606  pcopt2  20607  pcoass  20608  rrxcph  20908  ovoliunnul  21002  ovolicc1  21011  vitalilem5  21104  mbfpos  21141  0pval  21161  0pledm  21163  i1f1lem  21179  i1f1  21180  itg11  21181  itg1addlem3  21188  itg1addlem4  21189  i1fres  21195  itg1climres  21204  mbfi1fseqlem4  21208  mbfi1fseqlem6  21210  mbfi1flimlem  21212  mbfi1flim  21213  xrge0f  21221  itg2ge0  21225  itg2uba  21233  itg2splitlem  21238  itg2monolem1  21240  itg2gt0  21250  itg2cnlem1  21251  ibl0  21276  i1fibl  21297  itgeqa  21303  itgcn  21332  dvcmul  21430  dvcmulf  21431  dvexp3  21462  rolle  21474  dveq0  21484  dv11cn  21485  tdeglem4  21541  elply2  21676  elplyd  21682  ply1term  21684  ply0  21688  plyeq0  21691  plypf1  21692  plymullem  21696  dgrlt  21745  plymul0or  21759  dvply1  21762  plydivlem4  21774  elqaalem2  21798  aareccl  21804  aannenlem2  21807  tayl0  21839  taylpfval  21842  dvtaylp  21847  pserdvlem2  21905  abelthlem9  21917  logtayl  22117  leibpilem2  22348  leibpi  22349  jensenlem2  22393  jensen  22394  amgmlem  22395  amgm  22396  vmaval  22463  vmaf  22469  muval  22482  dchrelbas2  22588  dchrinvcl  22604  dchrptlem2  22616  lgseisenlem4  22703  pntrlog2bndlem4  22841  pntrlog2bndlem5  22842  padicval  22878  padicabv  22891  ostth1  22894  axlowdimlem8  23207  axlowdimlem9  23208  axlowdimlem10  23209  axlowdimlem11  23210  axlowdimlem12  23211  axlowdimlem13  23212  axlowdimlem17  23216  2trllemA  23461  2trllemH  23463  2trllemE  23464  2wlklemA  23465  wlkntrllem1  23470  wlkntrllem2  23471  wlkntrllem3  23472  2wlklem  23475  0spth  23482  constr1trl  23499  1pthon  23502  2pthlem2  23507  2wlklem1  23508  2pthon  23513  2pthon3v  23515  constr3lem2  23544  constr3lem4  23545  constr3lem5  23546  constr3trllem1  23548  constr3trllem2  23549  eupath  23614  occllem  24718  0cnfn  25396  0lnfn  25401  nmfn0  25403  nmcexi  25442  nlelchi  25477  sgnsval  26203  sgnsf  26204  xrge0iif1  26380  xrge0mulc1cn  26383  esumpfinval  26536  esumpfinvalf  26537  ddeval1  26662  ddeval0  26663  eulerpartlemt  26766  coinfliprv  26877  sgncl  26933  plymul02  26959  plymulx  26961  signsw0glem  26966  signsw0g  26969  signswmnd  26970  signswrid  26971  signstfvn  26982  igamval  27045  cvmliftlem4  27189  cvmliftlem5  27190  relexp0  27343  mblfinlem2  28441  mblfinlem3  28442  ismblfin  28444  itg2addnclem  28455  itg2addnclem3  28457  itg2addnc  28458  ftc1anclem3  28481  ftc1anclem5  28483  ftc1anclem7  28485  ftc1anclem8  28486  ftc1anc  28487  dvacos  28493  prdsbnd  28704  heiborlem10  28731  diophrw  29109  monotoddzzfi  29295  zindbi  29299  mncn0  29508  aaitgo  29531  flcidc  29543  ofsubid  29610  lhe4.4ex1a  29615  dvsconst  29616  dvconstbi  29620  climrec  29788  stoweidlem55  29862  wwlktovf1  30264  usgra2pthspth  30307  usgra2wlkspthlem1  30308  usgra2wlkspthlem2  30309  usgra2pthlem1  30312  usgra2pth  30313  usgra2adedglem1  30320  usg2wlkonot  30414  usg2wotspth  30415  clwwlkn2  30450  0egra0rgra  30561  rusgranumwlkl1  30571  zlmodzxzel  30764  zlmodzxz0  30765  zlmodzxzscm  30766  zlmodzxzadd  30767  idpmattoidmply1  30927  zlmodzxznm  31051  zlmodzxzldeplem  31052  zlmodzxzldeplem2  31055  ex-gt  31075  ex-gte  31076  renegclALT  32626
  Copyright terms: Public domain W3C validator