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

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

Proof of Theorem c0ex
StepHypRef Expression
1 0cn 10313 . 2 0 ∈ ℂ
21elexi 3407 1 0 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2156  Vcvv 3391  cc 10215  0cc0 10217
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-12 2214  ax-ext 2784  ax-1cn 10275  ax-icn 10276  ax-addcl 10277  ax-mulcl 10279  ax-i2m1 10285
This theorem depends on definitions:  df-bi 198  df-an 385  df-tru 1641  df-ex 1860  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-v 3393
This theorem is referenced by:  ofsubeq0  11298  ofsubge0  11300  elnn0  11557  un0mulcl  11589  frnnn0supp  11611  frnnn0fsupp  11612  nn0ssz  11660  nn0ind-raph  11739  xaddval  12268  xmulval  12270  ser0f  13073  facnn  13278  fac0  13279  bcval  13307  prhash2ex  13400  wrdexb  13523  s1rn  13590  eqs1  13603  repsw1  13750  cshw1  13788  s1co  13799  funcnvs2  13878  funcnvs3  13879  funcnvs4  13880  wrdlen2i  13907  wrd2pr2op  13908  wrd3tpop  13912  wwlktovf1  13921  wrdl3s3  13926  sgnval  14047  iserge0  14610  sum0  14671  sumz  14672  fsumss  14675  fsumser  14680  isumless  14795  geomulcvg  14825  rpnnen2lem1  15159  ruclem4  15179  ruclem8  15182  ruclem11  15185  0bits  15376  gcdval  15433  lcmval  15520  lcmfpr  15555  lcmfunsnlem2  15568  prmreclem2  15834  prmreclem5  15837  vdwapun  15891  mgmnsgrpex  17619  odval  18150  odf  18153  gexval  18190  telgsumfz0  18587  telgsum  18589  srgbinom  18743  abvtrivd  19040  snifpsrbag  19571  psrbaglesupp  19573  psrbagaddcl  19575  psrbaglefi  19577  mplcoe5  19673  mplbas2  19675  ltbwe  19677  psrbag0  19698  psrbagev1  19714  cply1coe0bi  19874  m2cpminvid2lem  20769  pmatcollpw3fi1lem1  20801  pmatcollpw3fi1lem2  20802  pmatcollpw3fi1  20803  idpm2idmp  20816  prdsdsf  22382  prdsxmetlem  22383  prdsmet  22385  imasdsf1olem  22388  prdsbl  22506  xrge0gsumle  22846  xrge0tsms  22847  xrhmeo  22955  pcopt  23031  pcopt2  23032  pcoass  23033  rrxcph  23391  ovoliunnul  23487  ovolicc1  23496  vitalilem5  23592  mbfpos  23631  0pval  23651  0pledm  23653  i1f1lem  23669  i1f1  23670  itg11  23671  itg1addlem3  23678  itg1addlem4  23679  i1fres  23685  itg1climres  23694  mbfi1fseqlem4  23698  mbfi1fseqlem6  23700  mbfi1flimlem  23702  mbfi1flim  23703  xrge0f  23711  itg2ge0  23715  itg2uba  23723  itg2splitlem  23728  itg2monolem1  23730  itg2gt0  23740  itg2cnlem1  23741  ibl0  23766  iblcnlem1  23767  i1fibl  23787  itgeqa  23793  itgcn  23822  dvcmul  23920  dvcmulf  23921  dvexp3  23954  rolle  23966  dveq0  23976  dv11cn  23977  tdeglem4  24033  elply2  24165  elplyd  24171  ply1term  24173  ply0  24177  plyeq0  24180  plypf1  24181  plymullem  24185  dgrlt  24235  plymul0or  24249  dvply1  24252  plydivlem4  24264  elqaalem2  24288  iaa  24293  aareccl  24294  aannenlem2  24297  tayl0  24329  taylpfval  24332  dvtaylp  24337  pserdvlem2  24395  abelthlem9  24407  logtayl  24619  cxplogb  24737  leibpilem2  24881  leibpi  24882  jensenlem2  24927  jensen  24928  amgmlem  24929  amgm  24930  igamval  24986  vmaval  25052  vmaf  25058  muval  25071  dchrelbas2  25175  dchrinvcl  25191  dchrptlem2  25203  lgseisenlem4  25316  pntrlog2bndlem4  25482  pntrlog2bndlem5  25483  padicval  25519  padicabv  25532  ostth1  25535  axlowdimlem8  26042  axlowdimlem9  26043  axlowdimlem10  26044  axlowdimlem11  26045  axlowdimlem12  26046  axlowdimlem13  26047  axlowdimlem17  26051  uspgr1ewop  26355  usgr2v1e2w  26359  umgr2v2eedg  26647  umgr2v2e  26648  umgr2v2evd2  26650  wlkl1loop  26761  2wlklem  26790  usgr2trlncl  26883  2wlkdlem4  27067  2wlkdlem5  27068  2pthdlem1  27069  2wlkdlem10  27074  umgrwwlks2on  27097  rusgrnumwwlkl1  27109  clwwlkn2  27192  0spth  27298  1wlkdlem4  27312  wlk2v2elem1  27327  3wlkdlem4  27334  3wlkdlem5  27335  3pthdlem1  27336  3wlkdlem10  27341  upgr3v3e3cycl  27352  upgr4cycl4dv4e  27357  eulerpathpr  27412  konigsberglem4  27427  konigsberglem5  27428  wlkl0  27546  occllem  28489  0cnfn  29166  0lnfn  29171  nmfn0  29173  nmcexi  29212  nlelchi  29247  fprodex01  29897  sgnsval  30052  sgnsf  30053  xrge0tsmsd  30109  xrge0iif1  30308  xrge0mulc1cn  30311  gsumesum  30445  esumpfinval  30461  esumpfinvalf  30462  ddeval1  30621  ddeval0  30622  ddemeas  30623  eulerpartlemt  30757  coinfliprv  30868  sgncl  30924  plymul02  30947  plymulx  30949  signsw0glem  30954  signsw0g  30957  signswmnd  30958  signswrid  30959  signstfvn  30970  prodfzo03  31005  circlevma  31044  circlemethhgt  31045  hgt750lemg  31056  hgt750lemb  31058  hgt750lema  31059  hgt750leme  31060  tgoldbachgtde  31062  tgoldbachgt  31065  cvmliftlem4  31591  cvmliftlem5  31592  poimirlem1  33721  poimirlem2  33722  poimirlem3  33723  poimirlem4  33724  poimirlem5  33725  poimirlem6  33726  poimirlem7  33727  poimirlem11  33731  poimirlem12  33732  poimirlem16  33736  poimirlem17  33737  poimirlem19  33739  poimirlem20  33740  poimirlem22  33742  poimirlem23  33743  poimirlem24  33744  poimirlem25  33745  poimirlem28  33748  poimirlem29  33749  poimirlem31  33751  poimirlem32  33752  poimir  33753  broucube  33754  mblfinlem2  33758  mblfinlem3  33759  ismblfin  33761  itg2addnclem  33771  itg2addnclem3  33773  itg2addnc  33774  ftc1anclem3  33797  ftc1anclem5  33799  ftc1anclem7  33801  ftc1anclem8  33802  ftc1anc  33803  dvacos  33807  prdsbnd  33901  heiborlem10  33928  renegclALT  34740  diophrw  37821  monotoddzzfi  38005  zindbi  38009  mncn0  38207  aaitgo  38230  flcidc  38242  dfrcl4  38465  fvrcllb0d  38482  fvrcllb0da  38483  iunrelexp0  38491  corclrcl  38496  relexp0idm  38504  dfrtrcl4  38527  corcltrcl  38528  cotrclrcl  38531  ofsubid  39020  lhe4.4ex1a  39025  dvsconst  39026  dvconstbi  39030  binomcxplemnn0  39045  binomcxplemdvbinom  39049  binomcxplemnotnn0  39052  n0p  39699  climrec  40312  limsup10exlem  40481  dvnmptdivc  40630  dvnmul  40635  stoweidlem55  40748  fourierdlem62  40861  fourierdlem104  40903  fouriersw  40924  rrxbasefi  40979  ovnval2  41238  hoidmvval  41270  hoidmvlelem1  41288  fun2dmnopgexmpl  41871  el1fzopredsuc  41907  zlmodzxzel  42698  zlmodzxz0  42699  zlmodzxzscm  42700  zlmodzxzadd  42701  zlmodzxznm  42851  zlmodzxzldeplem  42852  zlmodzxzldeplem2  42855  blen0  42931  nn0sumshdiglemB  42979  ex-gt  43037  ex-gte  43038  aacllem  43115
  Copyright terms: Public domain W3C validator