Theorem c0ex 11201

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

Syntax hints:   ∈ wcel 2143  Vcvv 3455  ℂcc 11099  0cc0 11101

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-mulcl 11163  ax-i2m1 11169

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457

This theorem is referenced by:  0elpr01  11202  ofsubeq0  12216  ofsubge0  12218  elnn0  12507  un0mulcl  12539  fcdmnn0supp  12562  fcdmnn0fsupp  12563  fcdmnn0suppg  12564  fcdmnn0fsuppg  12565  nn0ssz  12615  nn0ind-raph  12697  xaddval  13250  xmulval  13252  ser0f  14093  facnn  14313  fac0  14314  bcval  14342  prhash2ex  14437  wrdexb  14564  s1rn  14639  eqs1  14652  repsw1  14822  cshw1  14861  s1co  14872  funcnvs2  14952  funcnvs3  14953  funcnvs4  14954  wrdlen2i  14981  wrd2pr2op  14982  wrd3tpop  14987  wwlktovf1  14996  wrdl3s3  15001  sgnval  15127  sgndm  15135  sgncl  15136  iserge0  15714  sum0  15774  sumz  15775  fsumss  15778  fsumser  15783  isumless  15901  geomulcvg  15932  rpnnen2lem1  16271  ruclem4  16291  ruclem8  16294  ruclem11  16297  0bits  16498  gcdval  16555  lcmval  16651  lcmfpr  16686  lcmfunsnlem2  16699  prmreclem2  16978  prmreclem5  16981  vdwapun  17035  smndex1n0mnd  18975  mgmnsgrpex  18994  odval  19605  odf  19608  gexval  19649  telgsumfz0  20063  telgsum  20065  srgbinom  20314  abvtrivd  20916  pzriprnglem4  21615  pzriprnglem5  21616  pzriprnglem7  21618  pzriprnglem9  21620  pzriprnglem10  21621  snifpsrbag  22051  psrbaglesupp  22053  psrbaglefi  22057  mplcoe5  22172  mplbas2  22174  ltbwe  22176  psrbag0  22194  psrbagev1  22209  mhpmulcl  22293  psdmplcl  22306  psdmvr  22313  cply1coe0bi  22443  m2cpminvid2lem  22892  pmatcollpw3fi1lem1  22924  pmatcollpw3fi1lem2  22925  pmatcollpw3fi1  22926  idpm2idmp  22939  prdsdsf  24505  prdsxmetlem  24506  prdsmet  24508  imasdsf1olem  24511  prdsbl  24629  xrge0gsumle  24972  xrge0tsms  24973  xrhmeo  25086  pcopt  25162  pcopt2  25163  pcoass  25164  rrxcph  25532  rrx0el  25538  rrxbasefi  25550  ovoliunnul  25647  ovolicc1  25656  vitalilem5  25752  mbfpos  25791  0pval  25811  0pledm  25813  i1f1lem  25829  itg11  25831  itg1addlem3  25838  itg1addlem4  25839  i1fres  25845  itg1climres  25854  mbfi1fseqlem4  25858  mbfi1fseqlem6  25860  mbfi1flimlem  25862  mbfi1flim  25863  xrge0f  25871  itg2ge0  25875  itg2uba  25883  itg2splitlem  25888  itg2monolem1  25890  itg2gt0  25900  itg2cnlem1  25901  ibl0  25927  iblcnlem1  25928  i1fibl  25948  itgeqa  25954  itgcn  25985  dvcmul  26084  dvcmulf  26085  dvexp3  26118  dvef  26120  rolle  26130  dveq0  26140  dv11cn  26141  tdeglem4  26198  elply2  26334  elplyd  26340  ply1term  26342  ply0  26346  plyeq0  26349  plypf1  26350  plymullem  26354  dgrlt  26404  plymul0or  26420  plymul02  26422  plymulidp  26424  dvply1  26426  plydivlem4  26438  elqaalem2  26462  iaa  26469  aareccl  26470  aannenlem2  26473  tayl0  26506  taylpfval  26509  dvtaylp  26514  pserdvlem2  26572  abelthlem9  26584  logtayl  26806  cxplogb  26932  leibpilem2  27087  leibpi  27088  jensenlem2  27133  jensen  27134  amgmlem  27135  amgm  27136  igamval  27192  vmaval  27258  vmaf  27264  muval  27277  dchrelbas2  27382  dchrinvcl  27398  dchrptlem2  27410  lgseisenlem4  27523  addsqnreup  27588  pntrlog2bndlem4  27725  pntrlog2bndlem5  27726  padicval  27762  padicabv  27775  ostth1  27778  axlowdimlem8  29280  axlowdimlem9  29281  axlowdimlem10  29282  axlowdimlem11  29283  axlowdimlem12  29284  axlowdimlem13  29285  axlowdimlem17  29289  uspgr1ewop  29579  usgr2v1e2w  29583  umgr2v2eedg  29855  umgr2v2e  29856  umgr2v2evd2  29858  wlkl1loop  29968  2wlklem  29996  usgr2trlncl  30090  2wlkdlem4  30258  2wlkdlem5  30259  2pthdlem1  30260  2wlkdlem10  30265  usgrwwlks2on  30288  umgrwwlks2on  30289  rusgrnumwwlkl1  30301  clwwlkn2  30376  0spth  30458  1wlkdlem4  30472  wlk2v2elem1  30487  3wlkdlem4  30494  3wlkdlem5  30495  3pthdlem1  30496  3wlkdlem10  30501  upgr3v3e3cycl  30512  upgr4cycl4dv4e  30517  eulerpathpr  30572  konigsberglem4  30587  konigsberglem5  30588  wlkl0  30699  occllem  31636  0cnfn  32313  0lnfn  32318  nmfn0  32320  nmcexi  32359  nlelchi  32394  fprodex01  33150  indsupp  33168  indfsd  33169  indfsid  33170  s2rnOLD  33245  s3rnOLD  33247  gsummulsubdishift1  33369  gsummulsubdishift2s  33372  xrge0tsmsd  33374  cyc2fv1  33422  cyc3evpm  33451  sgnsval  33462  sgnsf  33463  elrgspnlem1  33543  elrgspnlem4  33546  gsumind  33646  0mplrim  33885  selvply1rhmlema  33889  selvply1rhmlemb  33890  selvply1rhmlem1  33891  selvply1rhmlem2  33892  selvply1rhmlem4  33894  selvply1rhm0  33897  extvfvvcl  33906  extvfvcl  33907  esplyfval0  33935  esplysply  33942  esplyind  33946  vieta  33951  constrextdg2lem  34119  xrge0iif1  34309  xrge0mulc1cn  34312  gsumesum  34430  esumpfinval  34446  esumpfinvalf  34447  ddeval1  34605  ddeval0  34606  ddemeas  34607  eulerpartlemt  34742  coinfliprv  34854  signsw0glem  34921  signsw0g  34924  signswmnd  34925  signswrid  34926  prodfzo03  34971  circlevma  35010  circlemethhgt  35011  hgt750lemg  35022  hgt750lemb  35024  hgt750lema  35025  hgt750leme  35026  tgoldbachgtde  35028  tgoldbachgt  35031  cvmliftlem4  35761  cvmliftlem5  35762  poimirlem1  38253  poimirlem2  38254  poimirlem3  38255  poimirlem4  38256  poimirlem5  38257  poimirlem6  38258  poimirlem7  38259  poimirlem11  38263  poimirlem12  38264  poimirlem16  38268  poimirlem17  38269  poimirlem19  38271  poimirlem20  38272  poimirlem22  38274  poimirlem23  38275  poimirlem24  38276  poimirlem25  38277  poimirlem28  38280  poimirlem29  38281  poimirlem31  38283  poimirlem32  38284  poimir  38285  broucube  38286  mblfinlem2  38290  mblfinlem3  38291  ismblfin  38293  itg2addnclem  38303  itg2addnclem3  38305  itg2addnc  38306  ftc1anclem3  38327  ftc1anclem5  38329  ftc1anclem7  38331  ftc1anclem8  38332  ftc1anc  38333  dvacos  38337  prdsbnd  38425  heiborlem10  38452  renegclALT  39718  aks4d1p1p4  42819  aks6d1c7lem1  42928  0prjspnlem  43338  0prjspnrel  43342  diophrw  43473  monotoddzzfi  43652  zindbi  43656  mncn0  43849  aaitgo  43872  flcidc  43880  dfrcl4  44385  iunrelexp0  44411  corclrcl  44416  relexp0idm  44424  dfrtrcl4  44447  corcltrcl  44448  cotrclrcl  44451  ofsubid  45017  lhe4.4ex1a  45022  dvsconst  45023  dvconstbi  45027  binomcxplemnn0  45042  binomcxplemdvbinom  45046  binomcxplemnotnn0  45049  n0p  45748  climrec  46302  limsup10exlem  46469  dvnmptdivc  46635  dvnmul  46640  stoweidlem55  46752  fourierdlem62  46865  fourierdlem104  46907  fouriersw  46928  ovnval2  47242  hoidmvval  47274  lambert0  47607  tannpoly  47610  sinnpoly  47611  fun2dmnopgexmpl  48004  el1fzopredsuc  48046  cycl3grtrilem  48694  stgrusgra  48707  stgrnbgr0  48712  isubgr3stgrlem3  48716  isubgr3stgrlem7  48720  usgrexmpl1lem  48769  usgrexmpl1tri  48773  usgrexmpl2lem  48774  usgrexmpl2nb0  48779  usgrexmpl2nb1  48780  usgrexmpl2nb2  48781  usgrexmpl2nb3  48782  usgrexmpl2nb4  48783  usgrexmpl2nb5  48784  usgrexmpl2trifr  48785  opgpgvtx  48803  gpgedgvtx0  48809  gpgvtxedg0  48811  gpgvtxedg1  48812  gpgedgiov  48813  gpgedg2ov  48814  gpg5nbgrvtx03starlem1  48816  gpg5nbgrvtx03starlem2  48817  gpg5nbgrvtx03starlem3  48818  gpg5nbgrvtx13starlem1  48819  gpg5nbgrvtx13starlem3  48821  gpg3nbgrvtx0  48824  gpg3nbgrvtx0ALT  48825  gpg3nbgrvtx1  48826  gpgcubic  48827  gpg5nbgr3star  48829  gpg3kgrtriex  48837  gpgprismgr4cycllem2  48844  gpgprismgr4cycllem7  48849  pgnioedg1  48856  pgnioedg2  48857  pgnioedg3  48858  pgnioedg4  48859  pgnioedg5  48860  pgnbgreunbgrlem1  48861  pgnbgreunbgrlem2lem1  48862  pgnbgreunbgrlem2lem2  48863  pgnbgreunbgrlem2lem3  48864  pgnbgreunbgrlem3  48866  pgnbgreunbgrlem5lem3  48870  pgnbgreunbgrlem5  48871  pgnbgreunbgrlem6  48872  gpg5edgnedg  48878  nn0mnd  48927  zlmodzxzel  49118  zlmodzxz0  49119  zlmodzxzscm  49120  zlmodzxzadd  49121  zlmodzxznm  49260  zlmodzxzldeplem  49261  zlmodzxzldeplem2  49264  blen0  49335  nn0sumshdiglemB  49383  fv1arycl  49400  1arympt1  49401  1arympt1fv  49402  1arymaptf1  49405  1arymaptfo  49406  fv2arycl  49411  2arymptfv  49413  2arymaptf1  49416  2arymaptfo  49417  ehl2eudisval0  49488  2sphere0  49513  line2ylem  49514  line2  49515  line2x  49517  line2y  49518  ex-gt  50489  ex-gte  50490  aacllem  50584