Theorem c0ex 10350

Description: Zero is a set. (Contributed by David A. Wheeler, 7-Jul-2016.)

Assertion

Ref	Expression
c0ex	⊢ 0 ∈ V

Proof of Theorem c0ex

Step	Hyp	Ref	Expression
1		0cn 10348	. 2 ⊢ 0 ∈ ℂ
2	1	elexi 3430	1 ⊢ 0 ∈ V

Syntax hints:   ∈ wcel 2166  Vcvv 3414  ℂcc 10250  0cc0 10252

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-12 2222  ax-ext 2803  ax-1cn 10310  ax-icn 10311  ax-addcl 10312  ax-mulcl 10314  ax-i2m1 10320

This theorem depends on definitions:  df-bi 199  df-an 387  df-tru 1662  df-ex 1881  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-v 3416

This theorem is referenced by:  ofsubeq0  11347  ofsubge0  11349  elnn0  11620  un0mulcl  11654  frnnn0supp  11676  frnnn0fsupp  11677  nn0ssz  11726  nn0ind-raph  11805  xaddval  12342  xmulval  12344  ser0f  13148  facnn  13355  fac0  13356  bcval  13384  prhash2ex  13476  wrdexb  13585  s1rn  13659  eqs1  13672  repsw1  13899  cshw1  13943  s1co  13954  funcnvs2  14034  funcnvs3  14035  funcnvs4  14036  wrdlen2i  14063  wrd2pr2op  14064  wrd3tpop  14069  wwlktovf1  14079  wrdl3s3  14084  sgnval  14205  iserge0  14768  sum0  14829  sumz  14830  fsumss  14833  fsumser  14838  isumless  14951  geomulcvg  14981  rpnnen2lem1  15317  ruclem4  15337  ruclem8  15340  ruclem11  15343  0bits  15534  gcdval  15591  lcmval  15678  lcmfpr  15713  lcmfunsnlem2  15726  prmreclem2  15992  prmreclem5  15995  vdwapun  16049  mgmnsgrpex  17772  odval  18304  odf  18307  gexval  18344  telgsumfz0  18743  telgsum  18745  srgbinom  18899  abvtrivd  19196  snifpsrbag  19727  psrbaglesupp  19729  psrbagaddcl  19731  psrbaglefi  19733  mplcoe5  19829  mplbas2  19831  ltbwe  19833  psrbag0  19854  psrbagev1  19870  cply1coe0bi  20030  m2cpminvid2lem  20929  pmatcollpw3fi1lem1  20961  pmatcollpw3fi1lem2  20962  pmatcollpw3fi1  20963  idpm2idmp  20976  prdsdsf  22542  prdsxmetlem  22543  prdsmet  22545  imasdsf1olem  22548  prdsbl  22666  xrge0gsumle  23006  xrge0tsms  23007  xrhmeo  23115  pcopt  23191  pcopt2  23192  pcoass  23193  rrxcph  23560  rrx0el  23566  rrxbasefi  23578  ovoliunnul  23673  ovolicc1  23682  vitalilem5  23778  mbfpos  23817  0pval  23837  0pledm  23839  i1f1lem  23855  i1f1  23856  itg11  23857  itg1addlem3  23864  itg1addlem4  23865  i1fres  23871  itg1climres  23880  mbfi1fseqlem4  23884  mbfi1fseqlem6  23886  mbfi1flimlem  23888  mbfi1flim  23889  xrge0f  23897  itg2ge0  23901  itg2uba  23909  itg2splitlem  23914  itg2monolem1  23916  itg2gt0  23926  itg2cnlem1  23927  ibl0  23952  iblcnlem1  23953  i1fibl  23973  itgeqa  23979  itgcn  24008  dvcmul  24106  dvcmulf  24107  dvexp3  24140  rolle  24152  dveq0  24162  dv11cn  24163  tdeglem4  24219  elply2  24351  elplyd  24357  ply1term  24359  ply0  24363  plyeq0  24366  plypf1  24367  plymullem  24371  dgrlt  24421  plymul0or  24435  dvply1  24438  plydivlem4  24450  elqaalem2  24474  iaa  24479  aareccl  24480  aannenlem2  24483  tayl0  24515  taylpfval  24518  dvtaylp  24523  pserdvlem2  24581  abelthlem9  24593  logtayl  24805  cxplogb  24926  leibpilem2  25081  leibpi  25082  jensenlem2  25127  jensen  25128  amgmlem  25129  amgm  25130  igamval  25186  vmaval  25252  vmaf  25258  muval  25271  dchrelbas2  25375  dchrinvcl  25391  dchrptlem2  25403  lgseisenlem4  25516  pntrlog2bndlem4  25682  pntrlog2bndlem5  25683  padicval  25719  padicabv  25732  ostth1  25735  axlowdimlem8  26248  axlowdimlem9  26249  axlowdimlem10  26250  axlowdimlem11  26251  axlowdimlem12  26252  axlowdimlem13  26253  axlowdimlem17  26257  uspgr1ewop  26545  usgr2v1e2w  26549  umgr2v2eedg  26822  umgr2v2e  26823  umgr2v2evd2  26825  wlkl1loop  26935  2wlklem  26964  usgr2trlncl  27062  2wlkdlem4  27257  2wlkdlem5  27258  2pthdlem1  27259  2wlkdlem10  27264  umgrwwlks2on  27286  rusgrnumwwlkl1  27297  clwwlkn2  27389  0spth  27502  1wlkdlem4  27516  wlk2v2elem1  27531  3wlkdlem4  27538  3wlkdlem5  27539  3pthdlem1  27540  3wlkdlem10  27545  upgr3v3e3cycl  27556  upgr4cycl4dv4e  27561  eulerpathpr  27617  konigsberglem4  27634  konigsberglem5  27635  wlkl0  27770  occllem  28717  0cnfn  29394  0lnfn  29399  nmfn0  29401  nmcexi  29440  nlelchi  29475  fprodex01  30118  sgnsval  30273  sgnsf  30274  xrge0tsmsd  30330  xrge0iif1  30529  xrge0mulc1cn  30532  gsumesum  30666  esumpfinval  30682  esumpfinvalf  30683  ddeval1  30842  ddeval0  30843  ddemeas  30844  eulerpartlemt  30978  coinfliprv  31090  sgncl  31146  plymul02  31170  plymulx  31172  signsw0glem  31177  signsw0g  31180  signswmnd  31181  signswrid  31182  signstfvn  31193  prodfzo03  31230  circlevma  31269  circlemethhgt  31270  hgt750lemg  31281  hgt750lemb  31283  hgt750lema  31284  hgt750leme  31285  tgoldbachgtde  31287  tgoldbachgt  31290  cvmliftlem4  31816  cvmliftlem5  31817  poimirlem1  33954  poimirlem2  33955  poimirlem3  33956  poimirlem4  33957  poimirlem5  33958  poimirlem6  33959  poimirlem7  33960  poimirlem11  33964  poimirlem12  33965  poimirlem16  33969  poimirlem17  33970  poimirlem19  33972  poimirlem20  33973  poimirlem22  33975  poimirlem23  33976  poimirlem24  33977  poimirlem25  33978  poimirlem28  33981  poimirlem29  33982  poimirlem31  33984  poimirlem32  33985  poimir  33986  broucube  33987  mblfinlem2  33991  mblfinlem3  33992  ismblfin  33994  itg2addnclem  34004  itg2addnclem3  34006  itg2addnc  34007  ftc1anclem3  34030  ftc1anclem5  34032  ftc1anclem7  34034  ftc1anclem8  34035  ftc1anc  34036  dvacos  34040  prdsbnd  34134  heiborlem10  34161  renegclALT  35038  diophrw  38166  monotoddzzfi  38350  zindbi  38354  mncn0  38552  aaitgo  38575  flcidc  38587  dfrcl4  38809  fvrcllb0d  38826  fvrcllb0da  38827  iunrelexp0  38835  corclrcl  38840  relexp0idm  38848  dfrtrcl4  38871  corcltrcl  38872  cotrclrcl  38875  ofsubid  39363  lhe4.4ex1a  39368  dvsconst  39369  dvconstbi  39373  binomcxplemnn0  39388  binomcxplemdvbinom  39392  binomcxplemnotnn0  39395  n0p  40026  climrec  40630  limsup10exlem  40799  dvnmptdivc  40948  dvnmul  40953  stoweidlem55  41066  fourierdlem62  41179  fourierdlem104  41221  fouriersw  41242  ovnval2  41553  hoidmvval  41585  hoidmvlelem1  41603  fun2dmnopgexmpl  42187  el1fzopredsuc  42223  zlmodzxzel  42980  zlmodzxz0  42981  zlmodzxzscm  42982  zlmodzxzadd  42983  zlmodzxznm  43133  zlmodzxzldeplem  43134  zlmodzxzldeplem2  43137  blen0  43213  nn0sumshdiglemB  43261  2sphere0  43302  line2ylem  43303  line2  43304  line2x  43306  line2y  43307  ex-gt  43367  ex-gte  43368  aacllem  43443