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

Theorem c0ex 10613
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 10611 . 2 0 ∈ ℂ
21elexi 3492 1 0 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2114  Vcvv 3473  cc 10513  0cc0 10515
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2792  ax-1cn 10573  ax-icn 10574  ax-addcl 10575  ax-mulcl 10577  ax-i2m1 10583
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-v 3475
This theorem is referenced by:  ofsubeq0  11613  ofsubge0  11615  elnn0  11878  un0mulcl  11910  frnnn0supp  11932  frnnn0fsupp  11933  nn0ssz  11982  nn0ind-raph  12061  xaddval  12595  xmulval  12597  ser0f  13408  facnn  13620  fac0  13621  bcval  13649  prhash2ex  13745  wrdexb  13857  s1rn  13933  eqs1  13946  repsw1  14125  cshw1  14164  s1co  14175  funcnvs2  14255  funcnvs3  14256  funcnvs4  14257  wrdlen2i  14284  wrd2pr2op  14285  wrd3tpop  14290  wwlktovf1  14301  wrdl3s3  14306  sgnval  14427  iserge0  14997  sum0  15058  sumz  15059  fsumss  15062  fsumser  15067  isumless  15180  geomulcvg  15212  rpnnen2lem1  15547  ruclem4  15567  ruclem8  15570  ruclem11  15573  0bits  15766  gcdval  15823  lcmval  15914  lcmfpr  15949  lcmfunsnlem2  15962  prmreclem2  16231  prmreclem5  16234  vdwapun  16288  smndex1n0mnd  18056  mgmnsgrpex  18075  odval  18641  odf  18644  gexval  18682  telgsumfz0  19091  telgsum  19093  srgbinom  19274  abvtrivd  19587  snifpsrbag  20122  psrbaglesupp  20124  psrbagaddcl  20126  psrbaglefi  20128  mplcoe5  20225  mplbas2  20227  ltbwe  20229  psrbag0  20250  psrbagev1  20266  cply1coe0bi  20444  m2cpminvid2lem  21338  pmatcollpw3fi1lem1  21370  pmatcollpw3fi1lem2  21371  pmatcollpw3fi1  21372  idpm2idmp  21385  prdsdsf  22953  prdsxmetlem  22954  prdsmet  22956  imasdsf1olem  22959  prdsbl  23077  xrge0gsumle  23417  xrge0tsms  23418  xrhmeo  23530  pcopt  23606  pcopt2  23607  pcoass  23608  rrxcph  23975  rrx0el  23981  rrxbasefi  23993  ovoliunnul  24090  ovolicc1  24099  vitalilem5  24195  mbfpos  24234  0pval  24254  0pledm  24256  i1f1lem  24272  i1f1  24273  itg11  24274  itg1addlem3  24281  itg1addlem4  24282  i1fres  24288  itg1climres  24297  mbfi1fseqlem4  24301  mbfi1fseqlem6  24303  mbfi1flimlem  24305  mbfi1flim  24306  xrge0f  24314  itg2ge0  24318  itg2uba  24326  itg2splitlem  24331  itg2monolem1  24333  itg2gt0  24343  itg2cnlem1  24344  ibl0  24369  iblcnlem1  24370  i1fibl  24390  itgeqa  24396  itgcn  24427  dvcmul  24526  dvcmulf  24527  dvexp3  24560  dvef  24562  rolle  24572  dveq0  24582  dv11cn  24583  tdeglem4  24640  elply2  24772  elplyd  24778  ply1term  24780  ply0  24784  plyeq0  24787  plypf1  24788  plymullem  24792  dgrlt  24842  plymul0or  24856  dvply1  24859  plydivlem4  24871  elqaalem2  24895  iaa  24900  aareccl  24901  aannenlem2  24904  tayl0  24936  taylpfval  24939  dvtaylp  24944  pserdvlem2  25002  abelthlem9  25014  logtayl  25230  cxplogb  25351  leibpilem2  25506  leibpi  25507  jensenlem2  25552  jensen  25553  amgmlem  25554  amgm  25555  igamval  25611  vmaval  25677  vmaf  25683  muval  25696  dchrelbas2  25800  dchrinvcl  25816  dchrptlem2  25828  lgseisenlem4  25941  addsqnreup  26006  pntrlog2bndlem4  26143  pntrlog2bndlem5  26144  padicval  26180  padicabv  26193  ostth1  26196  axlowdimlem8  26722  axlowdimlem9  26723  axlowdimlem10  26724  axlowdimlem11  26725  axlowdimlem12  26726  axlowdimlem13  26727  axlowdimlem17  26731  uspgr1ewop  27017  usgr2v1e2w  27021  umgr2v2eedg  27293  umgr2v2e  27294  umgr2v2evd2  27296  wlkl1loop  27406  2wlklem  27436  usgr2trlncl  27528  2wlkdlem4  27693  2wlkdlem5  27694  2pthdlem1  27695  2wlkdlem10  27700  umgrwwlks2on  27722  rusgrnumwwlkl1  27733  clwwlkn2  27808  0spth  27890  1wlkdlem4  27904  wlk2v2elem1  27919  3wlkdlem4  27926  3wlkdlem5  27927  3pthdlem1  27928  3wlkdlem10  27933  upgr3v3e3cycl  27944  upgr4cycl4dv4e  27949  eulerpathpr  28004  konigsberglem4  28019  konigsberglem5  28020  wlkl0  28131  occllem  29065  0cnfn  29742  0lnfn  29747  nmfn0  29749  nmcexi  29788  nlelchi  29823  fprodex01  30528  s2rn  30607  s3rn  30609  xrge0tsmsd  30700  cyc2fv1  30771  cyc3fv1  30787  cyc3evpm  30800  sgnsval  30811  sgnsf  30812  xrge0iif1  31189  xrge0mulc1cn  31192  gsumesum  31326  esumpfinval  31342  esumpfinvalf  31343  ddeval1  31501  ddeval0  31502  ddemeas  31503  eulerpartlemt  31637  coinfliprv  31748  sgncl  31804  plymul02  31824  plymulx  31826  signsw0glem  31831  signsw0g  31834  signswmnd  31835  signswrid  31836  prodfzo03  31882  circlevma  31921  circlemethhgt  31922  hgt750lemg  31933  hgt750lemb  31935  hgt750lema  31936  hgt750leme  31937  tgoldbachgtde  31939  tgoldbachgt  31942  cvmliftlem4  32543  cvmliftlem5  32544  poimirlem1  34934  poimirlem2  34935  poimirlem3  34936  poimirlem4  34937  poimirlem5  34938  poimirlem6  34939  poimirlem7  34940  poimirlem11  34944  poimirlem12  34945  poimirlem16  34949  poimirlem17  34950  poimirlem19  34952  poimirlem20  34953  poimirlem22  34955  poimirlem23  34956  poimirlem24  34957  poimirlem25  34958  poimirlem28  34961  poimirlem29  34962  poimirlem31  34964  poimirlem32  34965  poimir  34966  broucube  34967  mblfinlem2  34971  mblfinlem3  34972  ismblfin  34974  itg2addnclem  34984  itg2addnclem3  34986  itg2addnc  34987  ftc1anclem3  35008  ftc1anclem5  35010  ftc1anclem7  35012  ftc1anclem8  35013  ftc1anc  35014  dvacos  35018  prdsbnd  35107  heiborlem10  35134  renegclALT  36135  0prjspnlem  39405  0prjspnrel  39406  diophrw  39493  monotoddzzfi  39676  zindbi  39680  mncn0  39876  aaitgo  39899  flcidc  39911  dfrcl4  40156  fvrcllb0d  40173  fvrcllb0da  40174  iunrelexp0  40182  corclrcl  40187  relexp0idm  40195  dfrtrcl4  40218  corcltrcl  40219  cotrclrcl  40222  ofsubid  40811  lhe4.4ex1a  40816  dvsconst  40817  dvconstbi  40821  binomcxplemnn0  40836  binomcxplemdvbinom  40840  binomcxplemnotnn0  40843  n0p  41460  climrec  42036  limsup10exlem  42205  dvnmptdivc  42371  dvnmul  42376  stoweidlem55  42488  fourierdlem62  42601  fourierdlem104  42643  fouriersw  42664  ovnval2  42975  hoidmvval  43007  fun2dmnopgexmpl  43631  el1fzopredsuc  43673  nn0mnd  44231  zlmodzxzel  44548  zlmodzxz0  44549  zlmodzxzscm  44550  zlmodzxzadd  44551  zlmodzxznm  44697  zlmodzxzldeplem  44698  zlmodzxzldeplem2  44701  blen0  44777  nn0sumshdiglemB  44825  ehl2eudisval0  44899  2sphere0  44924  line2ylem  44925  line2  44926  line2x  44928  line2y  44929  ex-gt  45014  ex-gte  45015  aacllem  45089
  Copyright terms: Public domain W3C validator