Theorem c0ex 11138

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 11136	. 2 ⊢ 0 ∈ ℂ
2	1	elexi 3452	1 ⊢ 0 ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3429  ℂcc 11036  0cc0 11038

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-mulcl 11100  ax-i2m1 11106

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431

This theorem is referenced by:  ofsubeq0  12156  ofsubge0  12158  elnn0  12439  un0mulcl  12471  fcdmnn0supp  12494  fcdmnn0fsupp  12495  fcdmnn0suppg  12496  fcdmnn0fsuppg  12497  nn0ssz  12547  nn0ind-raph  12629  xaddval  13175  xmulval  13177  ser0f  14017  facnn  14237  fac0  14238  bcval  14266  prhash2ex  14361  wrdexb  14487  s1rn  14562  eqs1  14575  repsw1  14745  cshw1  14784  s1co  14795  funcnvs2  14875  funcnvs3  14876  funcnvs4  14877  wrdlen2i  14904  wrd2pr2op  14905  wrd3tpop  14910  wwlktovf1  14919  wrdl3s3  14924  sgnval  15050  iserge0  15623  sum0  15683  sumz  15684  fsumss  15687  fsumser  15692  isumless  15810  geomulcvg  15841  rpnnen2lem1  16181  ruclem4  16201  ruclem8  16204  ruclem11  16207  0bits  16408  gcdval  16465  lcmval  16561  lcmfpr  16596  lcmfunsnlem2  16609  prmreclem2  16888  prmreclem5  16891  vdwapun  16945  smndex1n0mnd  18883  mgmnsgrpex  18902  odval  19509  odf  19512  gexval  19553  telgsumfz0  19967  telgsum  19969  srgbinom  20212  abvtrivd  20809  pzriprnglem4  21464  pzriprnglem5  21465  pzriprnglem7  21467  pzriprnglem9  21469  pzriprnglem10  21470  snifpsrbag  21900  psrbaglesupp  21902  psrbaglefi  21906  mplcoe5  22018  mplbas2  22020  ltbwe  22022  psrbag0  22040  psrbagev1  22055  mhpmulcl  22115  psdmplcl  22128  psdmvr  22135  cply1coe0bi  22267  m2cpminvid2lem  22719  pmatcollpw3fi1lem1  22751  pmatcollpw3fi1lem2  22752  pmatcollpw3fi1  22753  idpm2idmp  22766  prdsdsf  24332  prdsxmetlem  24333  prdsmet  24335  imasdsf1olem  24338  prdsbl  24456  xrge0gsumle  24799  xrge0tsms  24800  xrhmeo  24913  pcopt  24989  pcopt2  24990  pcoass  24991  rrxcph  25359  rrx0el  25365  rrxbasefi  25377  ovoliunnul  25474  ovolicc1  25483  vitalilem5  25579  mbfpos  25618  0pval  25638  0pledm  25640  i1f1lem  25656  i1f1  25657  itg11  25658  itg1addlem3  25665  itg1addlem4  25666  i1fres  25672  itg1climres  25681  mbfi1fseqlem4  25685  mbfi1fseqlem6  25687  mbfi1flimlem  25689  mbfi1flim  25690  xrge0f  25698  itg2ge0  25702  itg2uba  25710  itg2splitlem  25715  itg2monolem1  25717  itg2gt0  25727  itg2cnlem1  25728  ibl0  25754  iblcnlem1  25755  i1fibl  25775  itgeqa  25781  itgcn  25812  dvcmul  25911  dvcmulf  25912  dvexp3  25945  dvef  25947  rolle  25957  dveq0  25967  dv11cn  25968  tdeglem4  26025  elply2  26161  elplyd  26167  ply1term  26169  ply0  26173  plyeq0  26176  plypf1  26177  plymullem  26181  dgrlt  26231  plymul0or  26247  dvply1  26250  plydivlem4  26262  elqaalem2  26286  iaa  26291  aareccl  26292  aannenlem2  26295  tayl0  26327  taylpfval  26330  dvtaylp  26335  pserdvlem2  26393  abelthlem9  26405  logtayl  26624  cxplogb  26750  leibpilem2  26905  leibpi  26906  jensenlem2  26951  jensen  26952  amgmlem  26953  amgm  26954  igamval  27010  vmaval  27076  vmaf  27082  muval  27095  dchrelbas2  27200  dchrinvcl  27216  dchrptlem2  27228  lgseisenlem4  27341  addsqnreup  27406  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  padicval  27580  padicabv  27593  ostth1  27596  axlowdimlem8  29018  axlowdimlem9  29019  axlowdimlem10  29020  axlowdimlem11  29021  axlowdimlem12  29022  axlowdimlem13  29023  axlowdimlem17  29027  uspgr1ewop  29317  usgr2v1e2w  29321  umgr2v2eedg  29593  umgr2v2e  29594  umgr2v2evd2  29596  wlkl1loop  29706  2wlklem  29734  usgr2trlncl  29828  2wlkdlem4  29996  2wlkdlem5  29997  2pthdlem1  29998  2wlkdlem10  30003  usgrwwlks2on  30026  umgrwwlks2on  30027  rusgrnumwwlkl1  30039  clwwlkn2  30114  0spth  30196  1wlkdlem4  30210  wlk2v2elem1  30225  3wlkdlem4  30232  3wlkdlem5  30233  3pthdlem1  30234  3wlkdlem10  30239  upgr3v3e3cycl  30250  upgr4cycl4dv4e  30255  eulerpathpr  30310  konigsberglem4  30325  konigsberglem5  30326  wlkl0  30437  occllem  31374  0cnfn  32051  0lnfn  32056  nmfn0  32058  nmcexi  32097  nlelchi  32132  fprodex01  32898  sgncl  32904  indsupp  32927  indfsd  32928  indfsid  32929  s2rnOLD  33004  s3rnOLD  33006  gsummulsubdishift1  33129  gsummulsubdishift2s  33132  xrge0tsmsd  33134  cyc2fv1  33182  cyc3fv1  33198  cyc3evpm  33211  sgnsval  33222  sgnsf  33223  elrgspnlem1  33303  elrgspnlem4  33306  gsumind  33405  extvfvvcl  33679  extvfvcl  33680  esplyfval0  33708  esplysply  33715  esplyind  33719  vieta  33724  constr01  33886  constrss  33887  constrconj  33889  constrextdg2lem  33892  nn0constr  33905  xrge0iif1  34082  xrge0mulc1cn  34085  gsumesum  34203  esumpfinval  34219  esumpfinvalf  34220  ddeval1  34378  ddeval0  34379  ddemeas  34380  eulerpartlemt  34515  coinfliprv  34627  plymul02  34690  plymulx  34692  signsw0glem  34697  signsw0g  34700  signswmnd  34701  signswrid  34702  prodfzo03  34747  circlevma  34786  circlemethhgt  34787  hgt750lemg  34798  hgt750lemb  34800  hgt750lema  34801  hgt750leme  34802  tgoldbachgtde  34804  tgoldbachgt  34807  cvmliftlem4  35470  cvmliftlem5  35471  poimirlem1  37942  poimirlem2  37943  poimirlem3  37944  poimirlem4  37945  poimirlem5  37946  poimirlem6  37947  poimirlem7  37948  poimirlem11  37952  poimirlem12  37953  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem22  37963  poimirlem23  37964  poimirlem24  37965  poimirlem25  37966  poimirlem28  37969  poimirlem29  37970  poimirlem31  37972  poimirlem32  37973  poimir  37974  broucube  37975  mblfinlem2  37979  mblfinlem3  37980  ismblfin  37982  itg2addnclem  37992  itg2addnclem3  37994  itg2addnc  37995  ftc1anclem3  38016  ftc1anclem5  38018  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  dvacos  38026  prdsbnd  38114  heiborlem10  38141  renegclALT  39409  aks4d1p1p4  42510  aks6d1c7lem1  42619  0prjspnlem  43056  0prjspnrel  43060  diophrw  43191  monotoddzzfi  43370  zindbi  43374  mncn0  43567  aaitgo  43590  flcidc  43598  dfrcl4  44103  fvrcllb0d  44120  fvrcllb0da  44121  iunrelexp0  44129  corclrcl  44134  relexp0idm  44142  dfrtrcl4  44165  corcltrcl  44166  cotrclrcl  44169  ofsubid  44751  lhe4.4ex1a  44756  dvsconst  44757  dvconstbi  44761  binomcxplemnn0  44776  binomcxplemdvbinom  44780  binomcxplemnotnn0  44783  n0p  45476  climrec  46033  limsup10exlem  46200  dvnmptdivc  46366  dvnmul  46371  stoweidlem55  46483  fourierdlem62  46596  fourierdlem104  46638  fouriersw  46659  ovnval2  46973  hoidmvval  47005  lambert0  47335  tannpoly  47338  sinnpoly  47339  fun2dmnopgexmpl  47732  el1fzopredsuc  47774  cycl3grtrilem  48422  stgrusgra  48435  stgr1  48437  stgrnbgr0  48440  isubgr3stgrlem3  48444  isubgr3stgrlem7  48448  usgrexmpl1lem  48497  usgrexmpl1tri  48501  usgrexmpl2lem  48502  usgrexmpl2nb0  48507  usgrexmpl2nb1  48508  usgrexmpl2nb2  48509  usgrexmpl2nb3  48510  usgrexmpl2nb4  48511  usgrexmpl2nb5  48512  usgrexmpl2trifr  48513  gpgiedgdmellem  48522  gpgvtx0  48529  opgpgvtx  48531  gpgedgvtx0  48537  gpgvtxedg0  48539  gpgvtxedg1  48540  gpgedgiov  48541  gpgedg2ov  48542  gpg5nbgrvtx03starlem1  48544  gpg5nbgrvtx03starlem2  48545  gpg5nbgrvtx03starlem3  48546  gpg5nbgrvtx13starlem1  48547  gpg5nbgrvtx13starlem3  48549  gpg3nbgrvtx0  48552  gpg3nbgrvtx0ALT  48553  gpg3nbgrvtx1  48554  gpgcubic  48555  gpg5nbgr3star  48557  gpg3kgrtriex  48565  gpgprismgr4cycllem2  48572  gpgprismgr4cycllem3  48573  gpgprismgr4cycllem7  48577  gpgprismgr4cycllem9  48579  pgnioedg1  48584  pgnioedg2  48585  pgnioedg3  48586  pgnioedg4  48587  pgnioedg5  48588  pgnbgreunbgrlem1  48589  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  pgnbgreunbgrlem2lem3  48592  pgnbgreunbgrlem3  48594  pgnbgreunbgrlem5lem3  48598  pgnbgreunbgrlem5  48599  pgnbgreunbgrlem6  48600  gpg5edgnedg  48606  nn0mnd  48655  zlmodzxzel  48831  zlmodzxz0  48832  zlmodzxzscm  48833  zlmodzxzadd  48834  zlmodzxznm  48973  zlmodzxzldeplem  48974  zlmodzxzldeplem2  48977  blen0  49048  nn0sumshdiglemB  49096  fv1arycl  49113  1arympt1  49114  1arympt1fv  49115  1arymaptf1  49118  1arymaptfo  49119  fv2arycl  49124  2arympt  49125  2arymptfv  49126  2arymaptf1  49129  2arymaptfo  49130  ehl2eudisval0  49201  2sphere0  49226  line2ylem  49227  line2  49228  line2x  49230  line2y  49231  ex-gt  50203  ex-gte  50204  aacllem  50276