Theorem c0ex 11218

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

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3458  ℂcc 11116  0cc0 11118

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-1cn 11176  ax-icn 11177  ax-addcl 11178  ax-mulcl 11180  ax-i2m1 11186

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460

This theorem is used by:  0elpr01  11219  ofsubeq0  12233  ofsubge0  12235  elnn0  12524  un0mulcl  12556  fcdmnn0supp  12579  fcdmnn0fsupp  12580  fcdmnn0suppg  12581  fcdmnn0fsuppg  12582  nn0ssz  12632  nn0ind-raph  12714  xaddval  13267  xmulval  13269  ser0f  14111  facnn  14331  fac0  14332  bcval  14360  prhash2ex  14455  wrdexb  14582  s1rn  14658  eqs1  14672  repsw1  14846  cshw1  14885  s1co  14896  funcnvs2  14976  funcnvs3  14977  funcnvs4  14978  wrdlen2i  15005  wrd2pr2op  15006  wrd3tpop  15011  wwlktovf1  15020  wrdl3s3  15025  sgnval  15151  sgndm  15159  sgncl  15160  iserge0  15738  sum0  15798  sumz  15799  fsumss  15802  fsumser  15807  isumless  15925  geomulcvg  15956  rpnnen2lem1  16295  ruclem4  16315  ruclem8  16318  ruclem11  16321  0bits  16522  gcdval  16579  lcmval  16675  lcmfpr  16710  lcmfunsnlem2  16723  prmreclem2  17002  prmreclem5  17005  vdwapun  17059  smndex1n0mnd  19005  mgmnsgrpex  19024  odval  19635  odf  19638  gexval  19679  telgsumfz0  20093  telgsum  20095  srgbinom  20344  abvtrivd  20972  pzriprnglem4  21671  pzriprnglem5  21672  pzriprnglem7  21674  pzriprnglem9  21676  pzriprnglem10  21677  snifpsrbag  22107  psrbaglesupp  22109  psrbaglefi  22113  mplcoe5  22228  mplbas2  22230  ltbwe  22232  psrbag0  22250  psrbagev1  22265  mhpmulcl  22349  psdmplcl  22362  psdmvr  22369  cply1coe0bi  22499  m2cpminvid2lem  22948  pmatcollpw3fi1lem1  22980  pmatcollpw3fi1lem2  22981  pmatcollpw3fi1  22982  idpm2idmp  22995  prdsdsf  24561  prdsxmetlem  24562  prdsmet  24564  imasdsf1olem  24567  prdsbl  24685  xrge0gsumle  25028  xrge0tsms  25029  xrhmeo  25142  pcopt  25218  pcopt2  25219  pcoass  25220  rrxcph  25588  rrx0el  25594  rrxbasefi  25606  ovoliunnul  25703  ovolicc1  25712  vitalilem5  25808  mbfpos  25847  0pval  25867  0pledm  25869  i1f1lem  25885  itg11  25887  itg1addlem3  25894  itg1addlem4  25895  i1fres  25901  itg1climres  25910  mbfi1fseqlem4  25914  mbfi1fseqlem6  25916  mbfi1flimlem  25918  mbfi1flim  25919  xrge0f  25927  itg2ge0  25931  itg2uba  25939  itg2splitlem  25944  itg2monolem1  25946  itg2gt0  25956  itg2cnlem1  25957  ibl0  25983  iblcnlem1  25984  i1fibl  26004  itgeqa  26010  itgcn  26041  dvcmul  26140  dvcmulf  26141  dvexp3  26174  dvef  26176  rolle  26186  dveq0  26196  dv11cn  26197  tdeglem4  26254  elply2  26390  elplyd  26396  ply1term  26398  ply0  26402  plyeq0  26405  plypf1  26406  plymullem  26410  dgrlt  26460  plymul0or  26476  plymul02  26478  plymulidp  26480  dvply1  26482  plydivlem4  26494  elqaalem2  26518  iaa  26525  aareccl  26526  aannenlem2  26529  tayl0  26562  taylpfval  26565  dvtaylp  26570  pserdvlem2  26628  abelthlem9  26640  logtayl  26862  cxplogb  26988  leibpilem2  27143  leibpi  27144  jensenlem2  27189  jensen  27190  amgmlem  27191  amgm  27192  igamval  27248  vmaval  27314  vmaf  27320  muval  27333  dchrelbas2  27438  dchrinvcl  27454  dchrptlem2  27466  lgseisenlem4  27579  addsqnreup  27644  pntrlog2bndlem4  27781  pntrlog2bndlem5  27782  padicval  27818  padicabv  27831  ostth1  27834  axlowdimlem8  29336  axlowdimlem9  29337  axlowdimlem10  29338  axlowdimlem11  29339  axlowdimlem12  29340  axlowdimlem13  29341  axlowdimlem17  29345  uspgr1ewop  29635  usgr2v1e2w  29639  umgr2v2eedg  29911  umgr2v2e  29912  umgr2v2evd2  29914  wlkl1loop  30024  2wlklem  30052  usgr2trlncl  30146  2wlkdlem4  30314  2wlkdlem5  30315  2pthdlem1  30316  2wlkdlem10  30321  usgrwwlks2on  30344  umgrwwlks2on  30345  rusgrnumwwlkl1  30357  clwwlkn2  30432  0spth  30514  1wlkdlem4  30528  wlk2v2elem1  30543  3wlkdlem4  30550  3wlkdlem5  30551  3pthdlem1  30552  3wlkdlem10  30557  upgr3v3e3cycl  30568  upgr4cycl4dv4e  30573  eulerpathpr  30628  konigsberglem4  30643  konigsberglem5  30644  wlkl0  30755  occllem  31692  0cnfn  32369  0lnfn  32374  nmfn0  32376  nmcexi  32415  nlelchi  32450  fprodex01  33206  indsupp  33224  indfsd  33225  indfsid  33226  gsummulsubdishift1  33419  gsummulsubdishift2s  33422  xrge0tsmsd  33424  cyc2fv1  33472  cyc3evpm  33501  sgnsval  33512  sgnsf  33513  elrgspnlem1  33593  elrgspnlem4  33596  gsumind  33696  0mplrim  33935  selvply1rhmlema  33939  selvply1rhmlemb  33940  selvply1rhmlem1  33941  selvply1rhmlem2  33942  selvply1rhmlem4  33944  selvply1rhm0  33947  extvfvvcl  33956  extvfvcl  33957  esplyfval0  33985  esplysply  33992  esplyind  33996  vieta  34001  constrextdg2lem  34169  xrge0iif1  34359  xrge0mulc1cn  34362  gsumesum  34480  esumpfinval  34496  esumpfinvalf  34497  ddeval1  34655  ddeval0  34656  ddemeas  34657  eulerpartlemt  34792  coinfliprv  34904  signsw0glem  34971  signsw0g  34974  signswmnd  34975  signswrid  34976  prodfzo03  35021  circlevma  35060  circlemethhgt  35061  hgt750lemg  35072  hgt750lemb  35074  hgt750lema  35075  hgt750leme  35076  tgoldbachgtde  35078  tgoldbachgt  35081  cvmliftlem4  35800  cvmliftlem5  35801  poimirlem1  38312  poimirlem2  38313  poimirlem3  38314  poimirlem4  38315  poimirlem5  38316  poimirlem6  38317  poimirlem7  38318  poimirlem11  38322  poimirlem12  38323  poimirlem16  38327  poimirlem17  38328  poimirlem19  38330  poimirlem20  38331  poimirlem22  38333  poimirlem23  38334  poimirlem24  38335  poimirlem25  38336  poimirlem28  38339  poimirlem29  38340  poimirlem31  38342  poimirlem32  38343  poimir  38344  broucube  38345  mblfinlem2  38349  mblfinlem3  38350  ismblfin  38352  itg2addnclem  38362  itg2addnclem3  38364  itg2addnc  38365  ftc1anclem3  38386  ftc1anclem5  38388  ftc1anclem7  38390  ftc1anclem8  38391  ftc1anc  38392  dvacos  38396  prdsbnd  38484  heiborlem10  38511  renegclALT  39777  aks4d1p1p4  42878  aks6d1c7lem1  42987  0prjspnlem  43395  0prjspnrel  43399  diophrw  43530  monotoddzzfi  43709  zindbi  43713  mncn0  43906  aaitgo  43929  flcidc  43937  dfrcl4  44442  iunrelexp0  44468  corclrcl  44473  relexp0idm  44481  dfrtrcl4  44504  corcltrcl  44505  cotrclrcl  44508  ofsubid  45074  lhe4.4ex1a  45079  dvsconst  45080  dvconstbi  45084  binomcxplemnn0  45099  binomcxplemdvbinom  45103  binomcxplemnotnn0  45106  n0p  45805  climrec  46359  limsup10exlem  46526  dvnmptdivc  46692  dvnmul  46697  stoweidlem55  46809  fourierdlem62  46922  fourierdlem104  46964  fouriersw  46985  ovnval2  47299  hoidmvval  47331  lambert0  47664  tannpoly  47667  sinnpoly  47668  fun2dmnopgexmpl  48061  el1fzopredsuc  48103  cycl3grtrilem  48751  stgrusgra  48764  stgrnbgr0  48769  isubgr3stgrlem3  48773  isubgr3stgrlem7  48777  usgrexmpl1lem  48826  usgrexmpl1tri  48830  usgrexmpl2lem  48831  usgrexmpl2nb0  48836  usgrexmpl2nb1  48837  usgrexmpl2nb2  48838  usgrexmpl2nb3  48839  usgrexmpl2nb4  48840  usgrexmpl2nb5  48841  usgrexmpl2trifr  48842  opgpgvtx  48860  gpgedgvtx0  48866  gpgvtxedg0  48868  gpgvtxedg1  48869  gpgedgiov  48870  gpgedg2ov  48871  gpg5nbgrvtx03starlem1  48873  gpg5nbgrvtx03starlem2  48874  gpg5nbgrvtx03starlem3  48875  gpg5nbgrvtx13starlem1  48876  gpg5nbgrvtx13starlem3  48878  gpg3nbgrvtx0  48881  gpg3nbgrvtx0ALT  48882  gpg3nbgrvtx1  48883  gpgcubic  48884  gpg5nbgr3star  48886  gpg3kgrtriex  48894  gpgprismgr4cycllem2  48901  gpgprismgr4cycllem7  48906  pgnioedg1  48913  pgnioedg2  48914  pgnioedg3  48915  pgnioedg4  48916  pgnioedg5  48917  pgnbgreunbgrlem1  48918  pgnbgreunbgrlem2lem1  48919  pgnbgreunbgrlem2lem2  48920  pgnbgreunbgrlem2lem3  48921  pgnbgreunbgrlem3  48923  pgnbgreunbgrlem5lem3  48927  pgnbgreunbgrlem5  48928  pgnbgreunbgrlem6  48929  gpg5edgnedg  48935  nn0mnd  48984  zlmodzxzel  49175  zlmodzxz0  49176  zlmodzxzscm  49177  zlmodzxzadd  49178  zlmodzxznm  49317  zlmodzxzldeplem  49318  zlmodzxzldeplem2  49321  blen0  49392  nn0sumshdiglemB  49440  fv1arycl  49457  1arympt1  49458  1arympt1fv  49459  1arymaptf1  49462  1arymaptfo  49463  fv2arycl  49468  2arymptfv  49470  2arymaptf1  49473  2arymaptfo  49474  ehl2eudisval0  49545  2sphere0  49570  line2ylem  49571  line2  49572  line2x  49574  line2y  49575  ex-gt  50546  ex-gte  50547  aacllem  50661