Theorem c0ex 11113

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

Syntax hints:   ∈ wcel 2113  Vcvv 3437  ℂcc 11011  0cc0 11013

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-1cn 11071  ax-icn 11072  ax-addcl 11073  ax-mulcl 11075  ax-i2m1 11081

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439

This theorem is referenced by:  ofsubeq0  12129  ofsubge0  12131  elnn0  12390  un0mulcl  12422  fcdmnn0supp  12445  fcdmnn0fsupp  12446  fcdmnn0suppg  12447  fcdmnn0fsuppg  12448  nn0ssz  12498  nn0ind-raph  12579  xaddval  13124  xmulval  13126  ser0f  13964  facnn  14184  fac0  14185  bcval  14213  prhash2ex  14308  wrdexb  14434  s1rn  14509  eqs1  14522  repsw1  14692  cshw1  14731  s1co  14742  funcnvs2  14822  funcnvs3  14823  funcnvs4  14824  wrdlen2i  14851  wrd2pr2op  14852  wrd3tpop  14857  wwlktovf1  14866  wrdl3s3  14871  sgnval  14997  iserge0  15570  sum0  15630  sumz  15631  fsumss  15634  fsumser  15639  isumless  15754  geomulcvg  15785  rpnnen2lem1  16125  ruclem4  16145  ruclem8  16148  ruclem11  16151  0bits  16352  gcdval  16409  lcmval  16505  lcmfpr  16540  lcmfunsnlem2  16553  prmreclem2  16831  prmreclem5  16834  vdwapun  16888  smndex1n0mnd  18822  mgmnsgrpex  18841  odval  19448  odf  19451  gexval  19492  telgsumfz0  19906  telgsum  19908  srgbinom  20151  abvtrivd  20749  pzriprnglem4  21423  pzriprnglem5  21424  pzriprnglem7  21426  pzriprnglem9  21428  pzriprnglem10  21429  snifpsrbag  21859  psrbaglesupp  21861  psrbaglefi  21865  mplcoe5  21976  mplbas2  21978  ltbwe  21980  psrbag0  21998  psrbagev1  22013  mhpmulcl  22065  psdmplcl  22078  psdmvr  22085  cply1coe0bi  22218  m2cpminvid2lem  22670  pmatcollpw3fi1lem1  22702  pmatcollpw3fi1lem2  22703  pmatcollpw3fi1  22704  idpm2idmp  22717  prdsdsf  24283  prdsxmetlem  24284  prdsmet  24286  imasdsf1olem  24289  prdsbl  24407  xrge0gsumle  24750  xrge0tsms  24751  xrhmeo  24872  pcopt  24950  pcopt2  24951  pcoass  24952  rrxcph  25320  rrx0el  25326  rrxbasefi  25338  ovoliunnul  25436  ovolicc1  25445  vitalilem5  25541  mbfpos  25580  0pval  25600  0pledm  25602  i1f1lem  25618  i1f1  25619  itg11  25620  itg1addlem3  25627  itg1addlem4  25628  i1fres  25634  itg1climres  25643  mbfi1fseqlem4  25647  mbfi1fseqlem6  25649  mbfi1flimlem  25651  mbfi1flim  25652  xrge0f  25660  itg2ge0  25664  itg2uba  25672  itg2splitlem  25677  itg2monolem1  25679  itg2gt0  25689  itg2cnlem1  25690  ibl0  25716  iblcnlem1  25717  i1fibl  25737  itgeqa  25743  itgcn  25774  dvcmul  25875  dvcmulf  25876  dvexp3  25910  dvef  25912  rolle  25922  dveq0  25933  dv11cn  25934  tdeglem4  25993  elply2  26129  elplyd  26135  ply1term  26137  ply0  26141  plyeq0  26144  plypf1  26145  plymullem  26149  dgrlt  26200  plymul0or  26216  dvply1  26219  plydivlem4  26232  elqaalem2  26256  iaa  26261  aareccl  26262  aannenlem2  26265  tayl0  26297  taylpfval  26300  dvtaylp  26306  pserdvlem2  26366  abelthlem9  26378  logtayl  26597  cxplogb  26724  leibpilem2  26879  leibpi  26880  jensenlem2  26926  jensen  26927  amgmlem  26928  amgm  26929  igamval  26985  vmaval  27051  vmaf  27057  muval  27070  dchrelbas2  27176  dchrinvcl  27192  dchrptlem2  27204  lgseisenlem4  27317  addsqnreup  27382  pntrlog2bndlem4  27519  pntrlog2bndlem5  27520  padicval  27556  padicabv  27569  ostth1  27572  axlowdimlem8  28929  axlowdimlem9  28930  axlowdimlem10  28931  axlowdimlem11  28932  axlowdimlem12  28933  axlowdimlem13  28934  axlowdimlem17  28938  uspgr1ewop  29228  usgr2v1e2w  29232  umgr2v2eedg  29505  umgr2v2e  29506  umgr2v2evd2  29508  wlkl1loop  29618  2wlklem  29646  usgr2trlncl  29740  2wlkdlem4  29908  2wlkdlem5  29909  2pthdlem1  29910  2wlkdlem10  29915  usgrwwlks2on  29938  umgrwwlks2on  29939  rusgrnumwwlkl1  29951  clwwlkn2  30026  0spth  30108  1wlkdlem4  30122  wlk2v2elem1  30137  3wlkdlem4  30144  3wlkdlem5  30145  3pthdlem1  30146  3wlkdlem10  30151  upgr3v3e3cycl  30162  upgr4cycl4dv4e  30167  eulerpathpr  30222  konigsberglem4  30237  konigsberglem5  30238  wlkl0  30349  occllem  31285  0cnfn  31962  0lnfn  31967  nmfn0  31969  nmcexi  32008  nlelchi  32043  fprodex01  32813  sgncl  32819  indsupp  32855  indfsd  32856  indfsid  32857  s2rnOLD  32932  s3rnOLD  32934  xrge0tsmsd  33049  cyc2fv1  33097  cyc3fv1  33113  cyc3evpm  33126  sgnsval  33137  sgnsf  33138  elrgspnlem1  33216  elrgspnlem4  33219  gsumind  33317  extvfvvcl  33586  extvfvcl  33587  esplysply  33611  esplyind  33613  constr01  33776  constrss  33777  constrconj  33779  constrextdg2lem  33782  nn0constr  33795  xrge0iif1  33972  xrge0mulc1cn  33975  gsumesum  34093  esumpfinval  34109  esumpfinvalf  34110  ddeval1  34268  ddeval0  34269  ddemeas  34270  eulerpartlemt  34405  coinfliprv  34517  plymul02  34580  plymulx  34582  signsw0glem  34587  signsw0g  34590  signswmnd  34591  signswrid  34592  prodfzo03  34637  circlevma  34676  circlemethhgt  34677  hgt750lemg  34688  hgt750lemb  34690  hgt750lema  34691  hgt750leme  34692  tgoldbachgtde  34694  tgoldbachgt  34697  cvmliftlem4  35353  cvmliftlem5  35354  poimirlem1  37681  poimirlem2  37682  poimirlem3  37683  poimirlem4  37684  poimirlem5  37685  poimirlem6  37686  poimirlem7  37687  poimirlem11  37691  poimirlem12  37692  poimirlem16  37696  poimirlem17  37697  poimirlem19  37699  poimirlem20  37700  poimirlem22  37702  poimirlem23  37703  poimirlem24  37704  poimirlem25  37705  poimirlem28  37708  poimirlem29  37709  poimirlem31  37711  poimirlem32  37712  poimir  37713  broucube  37714  mblfinlem2  37718  mblfinlem3  37719  ismblfin  37721  itg2addnclem  37731  itg2addnclem3  37733  itg2addnc  37734  ftc1anclem3  37755  ftc1anclem5  37757  ftc1anclem7  37759  ftc1anclem8  37760  ftc1anc  37761  dvacos  37765  prdsbnd  37853  heiborlem10  37880  renegclALT  39082  aks4d1p1p4  42184  aks6d1c7lem1  42293  0prjspnlem  42741  0prjspnrel  42745  diophrw  42876  monotoddzzfi  43059  zindbi  43063  mncn0  43256  aaitgo  43279  flcidc  43287  dfrcl4  43793  fvrcllb0d  43810  fvrcllb0da  43811  iunrelexp0  43819  corclrcl  43824  relexp0idm  43832  dfrtrcl4  43855  corcltrcl  43856  cotrclrcl  43859  ofsubid  44441  lhe4.4ex1a  44446  dvsconst  44447  dvconstbi  44451  binomcxplemnn0  44466  binomcxplemdvbinom  44470  binomcxplemnotnn0  44473  n0p  45166  climrec  45727  limsup10exlem  45894  dvnmptdivc  46060  dvnmul  46065  stoweidlem55  46177  fourierdlem62  46290  fourierdlem104  46332  fouriersw  46353  ovnval2  46667  hoidmvval  46699  lambert0  47011  tannpoly  47014  sinnpoly  47015  fun2dmnopgexmpl  47408  el1fzopredsuc  47449  cycl3grtrilem  48070  stgrusgra  48083  stgr1  48085  stgrnbgr0  48088  isubgr3stgrlem3  48092  isubgr3stgrlem7  48096  usgrexmpl1lem  48145  usgrexmpl1tri  48149  usgrexmpl2lem  48150  usgrexmpl2nb0  48155  usgrexmpl2nb1  48156  usgrexmpl2nb2  48157  usgrexmpl2nb3  48158  usgrexmpl2nb4  48159  usgrexmpl2nb5  48160  usgrexmpl2trifr  48161  gpgiedgdmellem  48170  gpgvtx0  48177  opgpgvtx  48179  gpgedgvtx0  48185  gpgvtxedg0  48187  gpgvtxedg1  48188  gpgedgiov  48189  gpgedg2ov  48190  gpg5nbgrvtx03starlem1  48192  gpg5nbgrvtx03starlem2  48193  gpg5nbgrvtx03starlem3  48194  gpg5nbgrvtx13starlem1  48195  gpg5nbgrvtx13starlem3  48197  gpg3nbgrvtx0  48200  gpg3nbgrvtx0ALT  48201  gpg3nbgrvtx1  48202  gpgcubic  48203  gpg5nbgr3star  48205  gpg3kgrtriex  48213  gpgprismgr4cycllem2  48220  gpgprismgr4cycllem3  48221  gpgprismgr4cycllem7  48225  gpgprismgr4cycllem9  48227  pgnioedg1  48232  pgnioedg2  48233  pgnioedg3  48234  pgnioedg4  48235  pgnioedg5  48236  pgnbgreunbgrlem1  48237  pgnbgreunbgrlem2lem1  48238  pgnbgreunbgrlem2lem2  48239  pgnbgreunbgrlem2lem3  48240  pgnbgreunbgrlem3  48242  pgnbgreunbgrlem5lem3  48246  pgnbgreunbgrlem5  48247  pgnbgreunbgrlem6  48248  gpg5edgnedg  48254  nn0mnd  48303  zlmodzxzel  48479  zlmodzxz0  48480  zlmodzxzscm  48481  zlmodzxzadd  48482  zlmodzxznm  48622  zlmodzxzldeplem  48623  zlmodzxzldeplem2  48626  blen0  48697  nn0sumshdiglemB  48745  fv1arycl  48762  1arympt1  48763  1arympt1fv  48764  1arymaptf1  48767  1arymaptfo  48768  fv2arycl  48773  2arympt  48774  2arymptfv  48775  2arymaptf1  48778  2arymaptfo  48779  ehl2eudisval0  48850  2sphere0  48875  line2ylem  48876  line2  48877  line2x  48879  line2y  48880  ex-gt  49853  ex-gte  49854  aacllem  49926