Theorem c0ex 11330

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

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454  ℂcc 11228  0cc0 11230

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-1cn 11288  ax-icn 11289  ax-addcl 11290  ax-mulcl 11292  ax-i2m1 11298

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456

This theorem is used by:  0elpr01  11331  ofsubeq0  12347  ofsubge0  12349  elnn0  12638  un0mulcl  12670  fcdmnn0supp  12693  fcdmnn0fsupp  12694  fcdmnn0suppg  12695  fcdmnn0fsuppg  12696  nn0ssz  12746  nn0ind-raph  12829  xaddval  13383  xmulval  13385  ser0f  14228  facnn  14449  fac0  14450  bcval  14478  prhash2ex  14573  wrdexb  14700  s1rn  14776  eqs1  14791  repsw1  14965  cshw1  15004  s1co  15015  funcnvs2  15096  funcnvs3  15097  funcnvs4  15098  wrdlen2i  15125  wrd2pr2op  15126  wrd3tpop  15131  s3rex  15133  wwlktovf1  15142  wrdl3s3  15147  sgnval  15273  sgndm  15281  sgncl  15282  iserge0  15860  sum0  15919  sumz  15920  fsumss  15923  fsumser  15928  isumless  16046  geomulcvg  16077  rpnnen2lem1  16414  ruclem4  16434  ruclem8  16437  ruclem11  16440  0bits  16641  gcdval  16698  lcmval  16799  lcmfpr  16834  lcmfunsnlem2  16847  prmreclem2  17127  prmreclem5  17130  vdwapun  17184  smndex1n0mnd  19143  mgmnsgrpex  19162  odval  19781  odf  19784  gexval  19825  telgsumfz0  20239  telgsum  20241  srgbinom  20490  abvtrivd  21122  pzriprnglem4  21823  pzriprnglem5  21824  pzriprnglem7  21826  pzriprnglem9  21828  pzriprnglem10  21829  snifpsrbag  22261  psrbaglesupp  22263  psrbaglefi  22267  mplcoe5  22382  mplbas2  22384  ltbwe  22386  psrbag0  22404  psrbagev1  22419  mhpmulcl  22503  psdmplcl  22516  psdmvr  22523  cply1coe0bi  22653  m2cpminvid2lem  23105  pmatcollpw3fi1lem1  23137  pmatcollpw3fi1lem2  23138  pmatcollpw3fi1  23139  idpm2idmp  23152  prdsdsf  24719  prdsxmetlem  24720  prdsmet  24722  imasdsf1olem  24725  prdsbl  24843  xrge0gsumle  25186  xrge0tsms  25187  xrhmeo  25300  pcopt  25376  pcopt2  25377  pcoass  25378  rrxcph  25746  rrx0el  25752  rrxbasefi  25764  ehlbase  25769  ehl1eudis  25774  ehl2eudis  25776  ovoliunnul  25861  ovolicc1  25870  vitalilem5  25966  mbfpos  26005  0pval  26025  0pledm  26027  i1f1lem  26043  itg11  26045  itg1addlem3  26052  itg1addlem4  26053  i1fres  26059  itg1climres  26068  mbfi1fseqlem4  26072  mbfi1fseqlem6  26074  mbfi1flimlem  26076  mbfi1flim  26077  xrge0f  26085  itg2ge0  26089  itg2uba  26097  itg2splitlem  26102  itg2monolem1  26104  itg2gt0  26114  itg2cnlem1  26115  ibl0  26140  iblcnlem1  26141  i1fibl  26161  itgeqa  26167  itgcn  26198  dvcmul  26297  dvcmulf  26298  dvexp3  26331  dvef  26333  rolle  26343  dveq0  26353  dv11cn  26354  tdeglem4  26411  elply2  26547  elplyd  26553  ply1term  26555  ply0  26559  plyeq0  26563  plypf1  26564  plymullem  26568  dgrlt  26618  plymul0or  26632  plymul02  26634  plymulidp  26636  dvply1  26638  plydivlem4  26650  elqaalem2  26676  iaaOLD  26685  aareccl  26686  aannenlem2  26689  tayl0  26722  taylpfval  26725  dvtaylp  26730  pserdvlem2  26788  abelthlem9  26800  logtayl  27021  cxplogb  27147  leibpilem2  27302  leibpi  27303  jensenlem2  27348  jensen  27349  amgmlem  27350  amgm  27351  igamval  27407  vmaval  27473  vmaf  27479  muval  27492  dchrelbas2  27597  dchrinvcl  27613  dchrptlem2  27625  lgseisenlem4  27738  addsqnreup  27803  pntrlog2bndlem4  27940  pntrlog2bndlem5  27941  padicval  27977  padicabv  27990  ostth1  27993  elcgrabasi  29408  axlowdimlem8  29560  axlowdimlem9  29561  axlowdimlem10  29562  axlowdimlem11  29563  axlowdimlem12  29564  axlowdimlem13  29565  axlowdimlem17  29569  uspgr1ewop  29862  usgr2v1e2w  29866  umgr2v2eedg  30138  umgr2v2e  30139  umgr2v2evd2  30141  wlkl1loop  30251  2wlklem  30279  usgr2trlncl  30379  2wlkdlem4  30550  2wlkdlem5  30551  2pthdlem1  30552  2wlkdlem10  30557  usgrwwlks2on  30580  umgrwwlks2on  30581  rusgrnumwwlkl1  30593  clwwlkn2  30668  0spth  30750  1wlkdlem4  30764  wlk2v2elem1  30789  3wlkdlem4  30796  3wlkdlem5  30797  3pthdlem1  30798  3wlkdlem10  30803  upgr3v3e3cycl  30814  upgr4cycl4dv4e  30819  eulerpathpr  30874  konigsberglem4  30889  konigsberglem5  30890  wlkl0  31001  occllem  31938  0cnfn  32615  0lnfn  32620  nmfn0  32622  nmcexi  32661  nlelchi  32696  fprodex01  33489  indsupp  33507  indfsd  33508  indfsid  33509  gsummulsubdishift1  33705  gsummulsubdishift2s  33708  xrge0tsmsd  33710  cyc2fv1  33758  cyc3evpm  33787  sgnsval  33798  sgnsf  33799  elrgspnlem1  33879  elrgspnlem4  33882  gsumind  33990  0mplrim  34229  selvply1rhmlema  34233  selvply1rhmlemb  34234  selvply1rhmlem1  34235  selvply1rhmlem2  34236  selvply1rhmlem4  34238  selvply1rhm0  34241  extvfvvcl  34250  extvfvcl  34251  esplyfval0  34279  esplysply  34286  esplyind  34290  vieta  34295  constrextdg2lem  34463  xrge0iif1  34653  xrge0mulc1cn  34656  gsumesum  34774  esumpfinval  34790  esumpfinvalf  34791  ddeval1  34950  ddeval0  34951  ddemeas  34952  eulerpartlemt  35086  coinfliprv  35198  signsw0glem  35265  signsw0g  35268  signswmnd  35269  signswrid  35270  prodfzo03  35315  circlevma  35354  circlemethhgt  35355  hgt750lemg  35366  hgt750lemb  35368  hgt750lema  35369  hgt750leme  35370  tgoldbachgtde  35372  tgoldbachgt  35375  cvmliftlem4  36233  cvmliftlem5  36234  poimirlem1  38744  poimirlem2  38745  poimirlem3  38746  poimirlem4  38747  poimirlem5  38748  poimirlem6  38749  poimirlem7  38750  poimirlem11  38754  poimirlem12  38755  poimirlem16  38759  poimirlem17  38760  poimirlem19  38762  poimirlem20  38763  poimirlem22  38765  poimirlem23  38766  poimirlem24  38767  poimirlem25  38768  poimirlem28  38771  poimirlem29  38772  poimirlem31  38774  poimirlem32  38775  poimir  38776  broucube  38777  mblfinlem2  38781  mblfinlem3  38782  ismblfin  38784  itg2addnclem  38794  itg2addnclem3  38796  itg2addnc  38797  ftc1anclem3  38818  ftc1anclem5  38820  ftc1anclem7  38822  ftc1anclem8  38823  ftc1anc  38824  dvacos  38828  prdsbnd  38930  heiborlem10  38957  renegclALT  40223  aks4d1p1p4  43324  aks6d1c7lem1  43433  0prjspnlem  43866  0prjspnrel  43867  diophrw  43974  monotoddzzfi  44153  zindbi  44157  mncn0  44344  aaitgo  44367  flcidc  44375  dfrcl4  44879  iunrelexp0  44905  corclrcl  44910  relexp0idm  44918  dfrtrcl4  44941  corcltrcl  44942  cotrclrcl  44945  ofsubid  45511  lhe4.4ex1a  45516  dvsconst  45517  dvconstbi  45521  binomcxplemnn0  45536  binomcxplemdvbinom  45540  binomcxplemnotnn0  45543  n0p  46278  climrec  46830  limsup10exlem  46997  dvnmptdivc  47163  dvnmul  47168  stoweidlem55  47280  fourierdlem62  47393  fourierdlem104  47435  fouriersw  47456  ovnval2  47770  hoidmvval  47802  lambert0  48152  tannpoly  48155  sinnpoly  48156  fun2dmnopgexmpl  48569  el1fzopredsuc  48611  cycl3grtrilem  49259  stgrusgra  49272  stgrnbgr0  49277  isubgr3stgrlem3  49281  isubgr3stgrlem7  49285  usgrexmpl1lem  49334  usgrexmpl1tri  49338  usgrexmpl2lem  49339  usgrexmpl2nb0  49344  usgrexmpl2nb1  49345  usgrexmpl2nb2  49346  usgrexmpl2nb3  49347  usgrexmpl2nb4  49348  usgrexmpl2nb5  49349  usgrexmpl2trifr  49350  opgpgvtx  49368  gpgedgvtx0  49374  gpgvtxedg0  49376  gpgvtxedg1  49377  gpgedgiov  49378  gpgedg2ov  49379  gpg5nbgrvtx03starlem1  49381  gpg5nbgrvtx03starlem2  49382  gpg5nbgrvtx03starlem3  49383  gpg5nbgrvtx13starlem1  49384  gpg5nbgrvtx13starlem3  49386  gpg3nbgrvtx0  49389  gpg3nbgrvtx0ALT  49390  gpg3nbgrvtx1  49391  gpgcubic  49392  gpg5nbgr3star  49394  gpg3kgrtriex  49402  gpgprismgr4cycllem2  49409  gpgprismgr4cycllem7  49414  pgnioedg1  49421  pgnioedg2  49422  pgnioedg3  49423  pgnioedg4  49424  pgnioedg5  49425  pgnbgreunbgrlem1  49426  pgnbgreunbgrlem2lem1  49427  pgnbgreunbgrlem2lem2  49428  pgnbgreunbgrlem2lem3  49429  pgnbgreunbgrlem3  49431  pgnbgreunbgrlem5lem3  49435  pgnbgreunbgrlem5  49436  pgnbgreunbgrlem6  49437  gpg5edgnedg  49443  nn0mnd  49491  zlmodzxzel  49682  zlmodzxz0  49683  zlmodzxzscm  49684  zlmodzxzadd  49685  zlmodzxznm  49824  zlmodzxzldeplem  49825  zlmodzxzldeplem2  49828  blen0  49899  nn0sumshdiglemB  49947  fv1arycl  49964  1arympt1  49965  1arympt1fv  49966  1arymaptf1  49969  1arymaptfo  49970  fv2arycl  49975  2arymptfv  49977  2arymaptf1  49980  2arymaptfo  49981  rrx2pnecoorneor  50043  ehl2eudisval0  50053  rrx2line  50067  rrx2linest  50069  2sphere0  50077  line2ylem  50078  line2  50079  ex-gt  51111  ex-gte  51112  aacllem  51251