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

Theorem c0ex 9994
Description: 0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
Assertion
Ref Expression
c0ex 0 ∈ V

Proof of Theorem c0ex
StepHypRef Expression
1 0cn 9992 . 2 0 ∈ ℂ
21elexi 3203 1 0 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 1987  Vcvv 3190  cc 9894  0cc0 9896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-12 2044  ax-ext 2601  ax-1cn 9954  ax-icn 9955  ax-addcl 9956  ax-mulcl 9958  ax-i2m1 9964
This theorem depends on definitions:  df-bi 197  df-an 386  df-tru 1483  df-ex 1702  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-v 3192
This theorem is referenced by:  ofsubeq0  10977  ofsubge0  10979  elnn0  11254  un0mulcl  11287  frnnn0supp  11309  frnnn0fsupp  11310  nn0ssz  11358  nn0ind-raph  11437  xaddval  12013  xmulval  12015  ser0f  12810  facnn  13018  fac0  13019  bcval  13047  prhash2ex  13143  wrdexb  13271  s1rn  13334  eqs1  13347  repsw1  13483  cshw1  13521  s1co  13532  funcnvs2  13610  funcnvs3  13611  funcnvs4  13612  wrdlen2i  13636  wrd2pr2op  13637  wrd3tpop  13641  wwlktovf1  13650  wrdl3s3  13655  sgnval  13778  iserge0  14341  sum0  14401  sumz  14402  fsumss  14405  fsumser  14410  isumless  14521  geomulcvg  14551  rpnnen2lem1  14887  ruclem4  14907  ruclem8  14910  ruclem11  14913  0bits  15104  gcdval  15161  lcmval  15248  lcmfpr  15283  lcmfunsnlem2  15296  prmreclem2  15564  prmreclem5  15567  vdwapun  15621  mgmnsgrpex  17358  odval  17893  odf  17896  gexval  17933  telgsumfz0  18329  telgsum  18331  srgbinom  18485  abvtrivd  18780  snifpsrbag  19306  psrbaglesupp  19308  psrbagaddcl  19310  psrbaglefi  19312  mplcoe5  19408  mplbas2  19410  ltbwe  19412  psrbag0  19434  psrbagev1  19450  cply1coe0bi  19610  m2cpminvid2lem  20499  pmatcollpw3fi1lem1  20531  pmatcollpw3fi1lem2  20532  pmatcollpw3fi1  20533  idpm2idmp  20546  prdsdsf  22112  prdsxmetlem  22113  prdsmet  22115  imasdsf1olem  22118  prdsbl  22236  xrge0gsumle  22576  xrge0tsms  22577  xrhmeo  22685  pcopt  22762  pcopt2  22763  pcoass  22764  rrxcph  23120  ovoliunnul  23215  ovolicc1  23224  vitalilem5  23321  mbfpos  23358  0pval  23378  0pledm  23380  i1f1lem  23396  i1f1  23397  itg11  23398  itg1addlem3  23405  itg1addlem4  23406  i1fres  23412  itg1climres  23421  mbfi1fseqlem4  23425  mbfi1fseqlem6  23427  mbfi1flimlem  23429  mbfi1flim  23430  xrge0f  23438  itg2ge0  23442  itg2uba  23450  itg2splitlem  23455  itg2monolem1  23457  itg2gt0  23467  itg2cnlem1  23468  ibl0  23493  iblcnlem1  23494  i1fibl  23514  itgeqa  23520  itgcn  23549  dvcmul  23647  dvcmulf  23648  dvexp3  23679  rolle  23691  dveq0  23701  dv11cn  23702  tdeglem4  23758  elply2  23890  elplyd  23896  ply1term  23898  ply0  23902  plyeq0  23905  plypf1  23906  plymullem  23910  dgrlt  23960  plymul0or  23974  dvply1  23977  plydivlem4  23989  elqaalem2  24013  iaa  24018  aareccl  24019  aannenlem2  24022  tayl0  24054  taylpfval  24057  dvtaylp  24062  pserdvlem2  24120  abelthlem9  24132  logtayl  24340  cxplogb  24458  leibpilem2  24602  leibpi  24603  jensenlem2  24648  jensen  24649  amgmlem  24650  amgm  24651  igamval  24707  vmaval  24773  vmaf  24779  muval  24792  dchrelbas2  24896  dchrinvcl  24912  dchrptlem2  24924  lgseisenlem4  25037  pntrlog2bndlem4  25203  pntrlog2bndlem5  25204  padicval  25240  padicabv  25253  ostth1  25256  axlowdimlem8  25763  axlowdimlem9  25764  axlowdimlem10  25765  axlowdimlem11  25766  axlowdimlem12  25767  axlowdimlem13  25768  axlowdimlem17  25772  uspgr1ewop  26067  usgr2v1e2w  26071  umgr2v2eedg  26340  umgr2v2e  26341  umgr2v2evd2  26343  wlkl1loop  26437  2wlklem  26466  usgr2trlncl  26559  2wlkdlem4  26727  2wlkdlem5  26728  2pthdlem1  26729  2wlkdlem10  26734  umgrwwlks2on  26753  rusgrnumwwlkl1  26764  clwwlksn2  26810  0spth  26887  1wlkdlem4  26900  wlk2v2elem1  26915  3wlkdlem4  26922  3wlkdlem5  26923  3pthdlem1  26924  3wlkdlem10  26929  upgr3v3e3cycl  26940  upgr4cycl4dv4e  26945  eulerpathpr  27000  konigsberglem4  27017  konigsberglem5  27018  occllem  28050  0cnfn  28727  0lnfn  28732  nmfn0  28734  nmcexi  28773  nlelchi  28808  sgnsval  29555  sgnsf  29556  xrge0tsmsd  29612  xrge0iif1  29808  xrge0mulc1cn  29811  gsumesum  29944  esumpfinval  29960  esumpfinvalf  29961  ddeval1  30120  ddeval0  30121  ddemeas  30122  eulerpartlemt  30256  coinfliprv  30367  sgncl  30423  plymul02  30445  plymulx  30447  signsw0glem  30452  signsw0g  30455  signswmnd  30456  signswrid  30457  signstfvn  30468  cvmliftlem4  31031  cvmliftlem5  31032  poimirlem1  33081  poimirlem2  33082  poimirlem3  33083  poimirlem4  33084  poimirlem5  33085  poimirlem6  33086  poimirlem7  33087  poimirlem11  33091  poimirlem12  33092  poimirlem16  33096  poimirlem17  33097  poimirlem19  33099  poimirlem20  33100  poimirlem22  33102  poimirlem23  33103  poimirlem24  33104  poimirlem25  33105  poimirlem28  33108  poimirlem29  33109  poimirlem31  33111  poimirlem32  33112  poimir  33113  broucube  33114  mblfinlem2  33118  mblfinlem3  33119  ismblfin  33121  itg2addnclem  33132  itg2addnclem3  33134  itg2addnc  33135  ftc1anclem3  33158  ftc1anclem5  33160  ftc1anclem7  33162  ftc1anclem8  33163  ftc1anc  33164  dvacos  33168  prdsbnd  33263  heiborlem10  33290  renegclALT  33768  diophrw  36841  monotoddzzfi  37026  zindbi  37030  mncn0  37229  aaitgo  37252  flcidc  37264  dfrcl4  37488  fvrcllb0d  37505  fvrcllb0da  37506  iunrelexp0  37514  corclrcl  37519  relexp0idm  37527  dfrtrcl4  37550  corcltrcl  37551  cotrclrcl  37554  ofsubid  38044  lhe4.4ex1a  38049  dvsconst  38050  dvconstbi  38054  binomcxplemnn0  38069  binomcxplemdvbinom  38073  binomcxplemnotnn0  38076  n0p  38731  climrec  39271  dvnmptdivc  39490  dvnmul  39495  stoweidlem55  39609  fourierdlem62  39722  fourierdlem104  39764  fouriersw  39785  rrxbasefi  39840  ovnval2  40096  hoidmvval  40128  hoidmvlelem1  40146  fun2dmnopgexmpl  40630  el1fzopredsuc  40662  zlmodzxzel  41451  zlmodzxz0  41452  zlmodzxzscm  41453  zlmodzxzadd  41454  zlmodzxznm  41604  zlmodzxzldeplem  41605  zlmodzxzldeplem2  41608  blen0  41688  nn0sumshdiglemB  41736  ex-gt  41792  ex-gte  41793  aacllem  41880
  Copyright terms: Public domain W3C validator