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  34656  ddeval0  34657  ddemeas  34658  eulerpartlemt  34793  coinfliprv  34905  signsw0glem  34972  signsw0g  34975  signswmnd  34976  signswrid  34977  prodfzo03  35022  circlevma  35061  circlemethhgt  35062  hgt750lemg  35073  hgt750lemb  35075  hgt750lema  35076  hgt750leme  35077  tgoldbachgtde  35079  tgoldbachgt  35082  cvmliftlem4  35801  cvmliftlem5  35802  poimirlem1  38313  poimirlem2  38314  poimirlem3  38315  poimirlem4  38316  poimirlem5  38317  poimirlem6  38318  poimirlem7  38319  poimirlem11  38323  poimirlem12  38324  poimirlem16  38328  poimirlem17  38329  poimirlem19  38331  poimirlem20  38332  poimirlem22  38334  poimirlem23  38335  poimirlem24  38336  poimirlem25  38337  poimirlem28  38340  poimirlem29  38341  poimirlem31  38343  poimirlem32  38344  poimir  38345  broucube  38346  mblfinlem2  38350  mblfinlem3  38351  ismblfin  38353  itg2addnclem  38363  itg2addnclem3  38365  itg2addnc  38366  ftc1anclem3  38387  ftc1anclem5  38389  ftc1anclem7  38391  ftc1anclem8  38392  ftc1anc  38393  dvacos  38397  prdsbnd  38485  heiborlem10  38512  renegclALT  39778  aks4d1p1p4  42879  aks6d1c7lem1  42988  0prjspnlem  43396  0prjspnrel  43400  diophrw  43531  monotoddzzfi  43710  zindbi  43714  mncn0  43907  aaitgo  43930  flcidc  43938  dfrcl4  44443  iunrelexp0  44469  corclrcl  44474  relexp0idm  44482  dfrtrcl4  44505  corcltrcl  44506  cotrclrcl  44509  ofsubid  45075  lhe4.4ex1a  45080  dvsconst  45081  dvconstbi  45085  binomcxplemnn0  45100  binomcxplemdvbinom  45104  binomcxplemnotnn0  45107  n0p  45806  climrec  46360  limsup10exlem  46527  dvnmptdivc  46693  dvnmul  46698  stoweidlem55  46810  fourierdlem62  46923  fourierdlem104  46965  fouriersw  46986  ovnval2  47300  hoidmvval  47332  lambert0  47665  tannpoly  47668  sinnpoly  47669  fun2dmnopgexmpl  48062  el1fzopredsuc  48104  cycl3grtrilem  48752  stgrusgra  48765  stgrnbgr0  48770  isubgr3stgrlem3  48774  isubgr3stgrlem7  48778  usgrexmpl1lem  48827  usgrexmpl1tri  48831  usgrexmpl2lem  48832  usgrexmpl2nb0  48837  usgrexmpl2nb1  48838  usgrexmpl2nb2  48839  usgrexmpl2nb3  48840  usgrexmpl2nb4  48841  usgrexmpl2nb5  48842  usgrexmpl2trifr  48843  opgpgvtx  48861  gpgedgvtx0  48867  gpgvtxedg0  48869  gpgvtxedg1  48870  gpgedgiov  48871  gpgedg2ov  48872  gpg5nbgrvtx03starlem1  48874  gpg5nbgrvtx03starlem2  48875  gpg5nbgrvtx03starlem3  48876  gpg5nbgrvtx13starlem1  48877  gpg5nbgrvtx13starlem3  48879  gpg3nbgrvtx0  48882  gpg3nbgrvtx0ALT  48883  gpg3nbgrvtx1  48884  gpgcubic  48885  gpg5nbgr3star  48887  gpg3kgrtriex  48895  gpgprismgr4cycllem2  48902  gpgprismgr4cycllem7  48907  pgnioedg1  48914  pgnioedg2  48915  pgnioedg3  48916  pgnioedg4  48917  pgnioedg5  48918  pgnbgreunbgrlem1  48919  pgnbgreunbgrlem2lem1  48920  pgnbgreunbgrlem2lem2  48921  pgnbgreunbgrlem2lem3  48922  pgnbgreunbgrlem3  48924  pgnbgreunbgrlem5lem3  48928  pgnbgreunbgrlem5  48929  pgnbgreunbgrlem6  48930  gpg5edgnedg  48936  nn0mnd  48985  zlmodzxzel  49176  zlmodzxz0  49177  zlmodzxzscm  49178  zlmodzxzadd  49179  zlmodzxznm  49318  zlmodzxzldeplem  49319  zlmodzxzldeplem2  49322  blen0  49393  nn0sumshdiglemB  49441  fv1arycl  49458  1arympt1  49459  1arympt1fv  49460  1arymaptf1  49463  1arymaptfo  49464  fv2arycl  49469  2arymptfv  49471  2arymaptf1  49474  2arymaptfo  49475  ehl2eudisval0  49546  2sphere0  49571  line2ylem  49572  line2  49573  line2x  49575  line2y  49576  ex-gt  50547  ex-gte  50548  aacllem  50662