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 3465	1 ⊢ 0 ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3442  ℂ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 2709  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 2716  df-cleq 2729  df-clel 2812  df-v 3444

This theorem is referenced by:  ofsubeq0  12154  ofsubge0  12156  elnn0  12415  un0mulcl  12447  fcdmnn0supp  12470  fcdmnn0fsupp  12471  fcdmnn0suppg  12472  fcdmnn0fsuppg  12473  nn0ssz  12523  nn0ind-raph  12604  xaddval  13150  xmulval  13152  ser0f  13990  facnn  14210  fac0  14211  bcval  14239  prhash2ex  14334  wrdexb  14460  s1rn  14535  eqs1  14548  repsw1  14718  cshw1  14757  s1co  14768  funcnvs2  14848  funcnvs3  14849  funcnvs4  14850  wrdlen2i  14877  wrd2pr2op  14878  wrd3tpop  14883  wwlktovf1  14892  wrdl3s3  14897  sgnval  15023  iserge0  15596  sum0  15656  sumz  15657  fsumss  15660  fsumser  15665  isumless  15780  geomulcvg  15811  rpnnen2lem1  16151  ruclem4  16171  ruclem8  16174  ruclem11  16177  0bits  16378  gcdval  16435  lcmval  16531  lcmfpr  16566  lcmfunsnlem2  16579  prmreclem2  16857  prmreclem5  16860  vdwapun  16914  smndex1n0mnd  18849  mgmnsgrpex  18868  odval  19475  odf  19478  gexval  19519  telgsumfz0  19933  telgsum  19935  srgbinom  20178  abvtrivd  20777  pzriprnglem4  21451  pzriprnglem5  21452  pzriprnglem7  21454  pzriprnglem9  21456  pzriprnglem10  21457  snifpsrbag  21888  psrbaglesupp  21890  psrbaglefi  21894  mplcoe5  22007  mplbas2  22009  ltbwe  22011  psrbag0  22029  psrbagev1  22044  mhpmulcl  22104  psdmplcl  22117  psdmvr  22124  cply1coe0bi  22258  m2cpminvid2lem  22710  pmatcollpw3fi1lem1  22742  pmatcollpw3fi1lem2  22743  pmatcollpw3fi1  22744  idpm2idmp  22757  prdsdsf  24323  prdsxmetlem  24324  prdsmet  24326  imasdsf1olem  24329  prdsbl  24447  xrge0gsumle  24790  xrge0tsms  24791  xrhmeo  24912  pcopt  24990  pcopt2  24991  pcoass  24992  rrxcph  25360  rrx0el  25366  rrxbasefi  25378  ovoliunnul  25476  ovolicc1  25485  vitalilem5  25581  mbfpos  25620  0pval  25640  0pledm  25642  i1f1lem  25658  i1f1  25659  itg11  25660  itg1addlem3  25667  itg1addlem4  25668  i1fres  25674  itg1climres  25683  mbfi1fseqlem4  25687  mbfi1fseqlem6  25689  mbfi1flimlem  25691  mbfi1flim  25692  xrge0f  25700  itg2ge0  25704  itg2uba  25712  itg2splitlem  25717  itg2monolem1  25719  itg2gt0  25729  itg2cnlem1  25730  ibl0  25756  iblcnlem1  25757  i1fibl  25777  itgeqa  25783  itgcn  25814  dvcmul  25915  dvcmulf  25916  dvexp3  25950  dvef  25952  rolle  25962  dveq0  25973  dv11cn  25974  tdeglem4  26033  elply2  26169  elplyd  26175  ply1term  26177  ply0  26181  plyeq0  26184  plypf1  26185  plymullem  26189  dgrlt  26240  plymul0or  26256  dvply1  26259  plydivlem4  26272  elqaalem2  26296  iaa  26301  aareccl  26302  aannenlem2  26305  tayl0  26337  taylpfval  26340  dvtaylp  26346  pserdvlem2  26406  abelthlem9  26418  logtayl  26637  cxplogb  26764  leibpilem2  26919  leibpi  26920  jensenlem2  26966  jensen  26967  amgmlem  26968  amgm  26969  igamval  27025  vmaval  27091  vmaf  27097  muval  27110  dchrelbas2  27216  dchrinvcl  27232  dchrptlem2  27244  lgseisenlem4  27357  addsqnreup  27422  pntrlog2bndlem4  27559  pntrlog2bndlem5  27560  padicval  27596  padicabv  27609  ostth1  27612  axlowdimlem8  29034  axlowdimlem9  29035  axlowdimlem10  29036  axlowdimlem11  29037  axlowdimlem12  29038  axlowdimlem13  29039  axlowdimlem17  29043  uspgr1ewop  29333  usgr2v1e2w  29337  umgr2v2eedg  29610  umgr2v2e  29611  umgr2v2evd2  29613  wlkl1loop  29723  2wlklem  29751  usgr2trlncl  29845  2wlkdlem4  30013  2wlkdlem5  30014  2pthdlem1  30015  2wlkdlem10  30020  usgrwwlks2on  30043  umgrwwlks2on  30044  rusgrnumwwlkl1  30056  clwwlkn2  30131  0spth  30213  1wlkdlem4  30227  wlk2v2elem1  30242  3wlkdlem4  30249  3wlkdlem5  30250  3pthdlem1  30251  3wlkdlem10  30256  upgr3v3e3cycl  30267  upgr4cycl4dv4e  30272  eulerpathpr  30327  konigsberglem4  30342  konigsberglem5  30343  wlkl0  30454  occllem  31390  0cnfn  32067  0lnfn  32072  nmfn0  32074  nmcexi  32113  nlelchi  32148  fprodex01  32916  sgncl  32922  indsupp  32959  indfsd  32960  indfsid  32961  s2rnOLD  33036  s3rnOLD  33038  gsummulsubdishift1  33161  gsummulsubdishift2s  33164  xrge0tsmsd  33166  cyc2fv1  33214  cyc3fv1  33230  cyc3evpm  33243  sgnsval  33254  sgnsf  33255  elrgspnlem1  33335  elrgspnlem4  33338  gsumind  33437  extvfvvcl  33711  extvfvcl  33712  esplyfval0  33740  esplysply  33747  esplyind  33751  vieta  33756  constr01  33919  constrss  33920  constrconj  33922  constrextdg2lem  33925  nn0constr  33938  xrge0iif1  34115  xrge0mulc1cn  34118  gsumesum  34236  esumpfinval  34252  esumpfinvalf  34253  ddeval1  34411  ddeval0  34412  ddemeas  34413  eulerpartlemt  34548  coinfliprv  34660  plymul02  34723  plymulx  34725  signsw0glem  34730  signsw0g  34733  signswmnd  34734  signswrid  34735  prodfzo03  34780  circlevma  34819  circlemethhgt  34820  hgt750lemg  34831  hgt750lemb  34833  hgt750lema  34834  hgt750leme  34835  tgoldbachgtde  34837  tgoldbachgt  34840  cvmliftlem4  35501  cvmliftlem5  35502  poimirlem1  37866  poimirlem2  37867  poimirlem3  37868  poimirlem4  37869  poimirlem5  37870  poimirlem6  37871  poimirlem7  37872  poimirlem11  37876  poimirlem12  37877  poimirlem16  37881  poimirlem17  37882  poimirlem19  37884  poimirlem20  37885  poimirlem22  37887  poimirlem23  37888  poimirlem24  37889  poimirlem25  37890  poimirlem28  37893  poimirlem29  37894  poimirlem31  37896  poimirlem32  37897  poimir  37898  broucube  37899  mblfinlem2  37903  mblfinlem3  37904  ismblfin  37906  itg2addnclem  37916  itg2addnclem3  37918  itg2addnc  37919  ftc1anclem3  37940  ftc1anclem5  37942  ftc1anclem7  37944  ftc1anclem8  37945  ftc1anc  37946  dvacos  37950  prdsbnd  38038  heiborlem10  38065  renegclALT  39333  aks4d1p1p4  42435  aks6d1c7lem1  42544  0prjspnlem  42975  0prjspnrel  42979  diophrw  43110  monotoddzzfi  43293  zindbi  43297  mncn0  43490  aaitgo  43513  flcidc  43521  dfrcl4  44026  fvrcllb0d  44043  fvrcllb0da  44044  iunrelexp0  44052  corclrcl  44057  relexp0idm  44065  dfrtrcl4  44088  corcltrcl  44089  cotrclrcl  44092  ofsubid  44674  lhe4.4ex1a  44679  dvsconst  44680  dvconstbi  44684  binomcxplemnn0  44699  binomcxplemdvbinom  44703  binomcxplemnotnn0  44706  n0p  45399  climrec  45957  limsup10exlem  46124  dvnmptdivc  46290  dvnmul  46295  stoweidlem55  46407  fourierdlem62  46520  fourierdlem104  46562  fouriersw  46583  ovnval2  46897  hoidmvval  46929  lambert0  47241  tannpoly  47244  sinnpoly  47245  fun2dmnopgexmpl  47638  el1fzopredsuc  47679  cycl3grtrilem  48300  stgrusgra  48313  stgr1  48315  stgrnbgr0  48318  isubgr3stgrlem3  48322  isubgr3stgrlem7  48326  usgrexmpl1lem  48375  usgrexmpl1tri  48379  usgrexmpl2lem  48380  usgrexmpl2nb0  48385  usgrexmpl2nb1  48386  usgrexmpl2nb2  48387  usgrexmpl2nb3  48388  usgrexmpl2nb4  48389  usgrexmpl2nb5  48390  usgrexmpl2trifr  48391  gpgiedgdmellem  48400  gpgvtx0  48407  opgpgvtx  48409  gpgedgvtx0  48415  gpgvtxedg0  48417  gpgvtxedg1  48418  gpgedgiov  48419  gpgedg2ov  48420  gpg5nbgrvtx03starlem1  48422  gpg5nbgrvtx03starlem2  48423  gpg5nbgrvtx03starlem3  48424  gpg5nbgrvtx13starlem1  48425  gpg5nbgrvtx13starlem3  48427  gpg3nbgrvtx0  48430  gpg3nbgrvtx0ALT  48431  gpg3nbgrvtx1  48432  gpgcubic  48433  gpg5nbgr3star  48435  gpg3kgrtriex  48443  gpgprismgr4cycllem2  48450  gpgprismgr4cycllem3  48451  gpgprismgr4cycllem7  48455  gpgprismgr4cycllem9  48457  pgnioedg1  48462  pgnioedg2  48463  pgnioedg3  48464  pgnioedg4  48465  pgnioedg5  48466  pgnbgreunbgrlem1  48467  pgnbgreunbgrlem2lem1  48468  pgnbgreunbgrlem2lem2  48469  pgnbgreunbgrlem2lem3  48470  pgnbgreunbgrlem3  48472  pgnbgreunbgrlem5lem3  48476  pgnbgreunbgrlem5  48477  pgnbgreunbgrlem6  48478  gpg5edgnedg  48484  nn0mnd  48533  zlmodzxzel  48709  zlmodzxz0  48710  zlmodzxzscm  48711  zlmodzxzadd  48712  zlmodzxznm  48851  zlmodzxzldeplem  48852  zlmodzxzldeplem2  48855  blen0  48926  nn0sumshdiglemB  48974  fv1arycl  48991  1arympt1  48992  1arympt1fv  48993  1arymaptf1  48996  1arymaptfo  48997  fv2arycl  49002  2arympt  49003  2arymptfv  49004  2arymaptf1  49007  2arymaptfo  49008  ehl2eudisval0  49079  2sphere0  49104  line2ylem  49105  line2  49106  line2x  49108  line2y  49109  ex-gt  50081  ex-gte  50082  aacllem  50154