Theorem c0ex 11168

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

Syntax hints:   ∈ wcel 2109  Vcvv 3447  ℂcc 11066  0cc0 11068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-mulcl 11130  ax-i2m1 11136

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449

This theorem is referenced by:  ofsubeq0  12183  ofsubge0  12185  elnn0  12444  un0mulcl  12476  fcdmnn0supp  12499  fcdmnn0fsupp  12500  fcdmnn0suppg  12501  fcdmnn0fsuppg  12502  nn0ssz  12552  nn0ind-raph  12634  xaddval  13183  xmulval  13185  ser0f  14020  facnn  14240  fac0  14241  bcval  14269  prhash2ex  14364  wrdexb  14490  s1rn  14564  eqs1  14577  repsw1  14748  cshw1  14787  s1co  14799  funcnvs2  14879  funcnvs3  14880  funcnvs4  14881  wrdlen2i  14908  wrd2pr2op  14909  wrd3tpop  14914  wwlktovf1  14923  wrdl3s3  14928  sgnval  15054  iserge0  15627  sum0  15687  sumz  15688  fsumss  15691  fsumser  15696  isumless  15811  geomulcvg  15842  rpnnen2lem1  16182  ruclem4  16202  ruclem8  16205  ruclem11  16208  0bits  16409  gcdval  16466  lcmval  16562  lcmfpr  16597  lcmfunsnlem2  16610  prmreclem2  16888  prmreclem5  16891  vdwapun  16945  smndex1n0mnd  18839  mgmnsgrpex  18858  odval  19464  odf  19467  gexval  19508  telgsumfz0  19922  telgsum  19924  srgbinom  20140  abvtrivd  20741  pzriprnglem4  21394  pzriprnglem5  21395  pzriprnglem7  21397  pzriprnglem9  21399  pzriprnglem10  21400  snifpsrbag  21829  psrbaglesupp  21831  psrbaglefi  21835  mplcoe5  21947  mplbas2  21949  ltbwe  21951  psrbag0  21969  psrbagev1  21984  mhpmulcl  22036  psdmplcl  22049  psdmvr  22056  cply1coe0bi  22189  m2cpminvid2lem  22641  pmatcollpw3fi1lem1  22673  pmatcollpw3fi1lem2  22674  pmatcollpw3fi1  22675  idpm2idmp  22688  prdsdsf  24255  prdsxmetlem  24256  prdsmet  24258  imasdsf1olem  24261  prdsbl  24379  xrge0gsumle  24722  xrge0tsms  24723  xrhmeo  24844  pcopt  24922  pcopt2  24923  pcoass  24924  rrxcph  25292  rrx0el  25298  rrxbasefi  25310  ovoliunnul  25408  ovolicc1  25417  vitalilem5  25513  mbfpos  25552  0pval  25572  0pledm  25574  i1f1lem  25590  i1f1  25591  itg11  25592  itg1addlem3  25599  itg1addlem4  25600  i1fres  25606  itg1climres  25615  mbfi1fseqlem4  25619  mbfi1fseqlem6  25621  mbfi1flimlem  25623  mbfi1flim  25624  xrge0f  25632  itg2ge0  25636  itg2uba  25644  itg2splitlem  25649  itg2monolem1  25651  itg2gt0  25661  itg2cnlem1  25662  ibl0  25688  iblcnlem1  25689  i1fibl  25709  itgeqa  25715  itgcn  25746  dvcmul  25847  dvcmulf  25848  dvexp3  25882  dvef  25884  rolle  25894  dveq0  25905  dv11cn  25906  tdeglem4  25965  elply2  26101  elplyd  26107  ply1term  26109  ply0  26113  plyeq0  26116  plypf1  26117  plymullem  26121  dgrlt  26172  plymul0or  26188  dvply1  26191  plydivlem4  26204  elqaalem2  26228  iaa  26233  aareccl  26234  aannenlem2  26237  tayl0  26269  taylpfval  26272  dvtaylp  26278  pserdvlem2  26338  abelthlem9  26350  logtayl  26569  cxplogb  26696  leibpilem2  26851  leibpi  26852  jensenlem2  26898  jensen  26899  amgmlem  26900  amgm  26901  igamval  26957  vmaval  27023  vmaf  27029  muval  27042  dchrelbas2  27148  dchrinvcl  27164  dchrptlem2  27176  lgseisenlem4  27289  addsqnreup  27354  pntrlog2bndlem4  27491  pntrlog2bndlem5  27492  padicval  27528  padicabv  27541  ostth1  27544  axlowdimlem8  28876  axlowdimlem9  28877  axlowdimlem10  28878  axlowdimlem11  28879  axlowdimlem12  28880  axlowdimlem13  28881  axlowdimlem17  28885  uspgr1ewop  29175  usgr2v1e2w  29179  umgr2v2eedg  29452  umgr2v2e  29453  umgr2v2evd2  29455  wlkl1loop  29566  2wlklem  29595  usgr2trlncl  29690  2wlkdlem4  29858  2wlkdlem5  29859  2pthdlem1  29860  2wlkdlem10  29865  umgrwwlks2on  29887  rusgrnumwwlkl1  29898  clwwlkn2  29973  0spth  30055  1wlkdlem4  30069  wlk2v2elem1  30084  3wlkdlem4  30091  3wlkdlem5  30092  3pthdlem1  30093  3wlkdlem10  30098  upgr3v3e3cycl  30109  upgr4cycl4dv4e  30114  eulerpathpr  30169  konigsberglem4  30184  konigsberglem5  30185  wlkl0  30296  occllem  31232  0cnfn  31909  0lnfn  31914  nmfn0  31916  nmcexi  31955  nlelchi  31990  fprodex01  32750  sgncl  32756  indsupp  32790  s2rnOLD  32865  s3rnOLD  32867  xrge0tsmsd  33002  cyc2fv1  33078  cyc3fv1  33094  cyc3evpm  33107  sgnsval  33118  sgnsf  33119  elrgspnlem1  33193  elrgspnlem4  33196  constr01  33732  constrss  33733  constrconj  33735  constrextdg2lem  33738  nn0constr  33751  xrge0iif1  33928  xrge0mulc1cn  33931  gsumesum  34049  esumpfinval  34065  esumpfinvalf  34066  ddeval1  34224  ddeval0  34225  ddemeas  34226  eulerpartlemt  34362  coinfliprv  34474  plymul02  34537  plymulx  34539  signsw0glem  34544  signsw0g  34547  signswmnd  34548  signswrid  34549  prodfzo03  34594  circlevma  34633  circlemethhgt  34634  hgt750lemg  34645  hgt750lemb  34647  hgt750lema  34648  hgt750leme  34649  tgoldbachgtde  34651  tgoldbachgt  34654  cvmliftlem4  35275  cvmliftlem5  35276  poimirlem1  37615  poimirlem2  37616  poimirlem3  37617  poimirlem4  37618  poimirlem5  37619  poimirlem6  37620  poimirlem7  37621  poimirlem11  37625  poimirlem12  37626  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem22  37636  poimirlem23  37637  poimirlem24  37638  poimirlem25  37639  poimirlem28  37642  poimirlem29  37643  poimirlem31  37645  poimirlem32  37646  poimir  37647  broucube  37648  mblfinlem2  37652  mblfinlem3  37653  ismblfin  37655  itg2addnclem  37665  itg2addnclem3  37667  itg2addnc  37668  ftc1anclem3  37689  ftc1anclem5  37691  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  dvacos  37699  prdsbnd  37787  heiborlem10  37814  renegclALT  38956  aks4d1p1p4  42059  aks6d1c7lem1  42168  0prjspnlem  42611  0prjspnrel  42615  diophrw  42747  monotoddzzfi  42931  zindbi  42935  mncn0  43128  aaitgo  43151  flcidc  43159  dfrcl4  43665  fvrcllb0d  43682  fvrcllb0da  43683  iunrelexp0  43691  corclrcl  43696  relexp0idm  43704  dfrtrcl4  43727  corcltrcl  43728  cotrclrcl  43731  ofsubid  44313  lhe4.4ex1a  44318  dvsconst  44319  dvconstbi  44323  binomcxplemnn0  44338  binomcxplemdvbinom  44342  binomcxplemnotnn0  44345  n0p  45039  climrec  45601  limsup10exlem  45770  dvnmptdivc  45936  dvnmul  45941  stoweidlem55  46053  fourierdlem62  46166  fourierdlem104  46208  fouriersw  46229  ovnval2  46543  hoidmvval  46575  tworepnotupword  46884  lambert0  46888  tannpoly  46891  sinnpoly  46892  fun2dmnopgexmpl  47285  el1fzopredsuc  47326  cycl3grtrilem  47945  stgrusgra  47958  stgr1  47960  stgrnbgr0  47963  isubgr3stgrlem3  47967  isubgr3stgrlem7  47971  usgrexmpl1lem  48012  usgrexmpl1tri  48016  usgrexmpl2lem  48017  usgrexmpl2nb0  48022  usgrexmpl2nb1  48023  usgrexmpl2nb2  48024  usgrexmpl2nb3  48025  usgrexmpl2nb4  48026  usgrexmpl2nb5  48027  usgrexmpl2trifr  48028  gpgiedgdmellem  48037  gpgvtx0  48044  opgpgvtx  48046  gpgedgvtx0  48052  gpgvtxedg0  48054  gpgvtxedg1  48055  gpgedgiov  48056  gpgedg2ov  48057  gpg5nbgrvtx03starlem1  48059  gpg5nbgrvtx03starlem2  48060  gpg5nbgrvtx03starlem3  48061  gpg5nbgrvtx13starlem1  48062  gpg5nbgrvtx13starlem3  48064  gpg3nbgrvtx0  48067  gpg3nbgrvtx0ALT  48068  gpg3nbgrvtx1  48069  gpgcubic  48070  gpg5nbgr3star  48072  gpg3kgrtriex  48080  gpgprismgr4cycllem2  48086  gpgprismgr4cycllem3  48087  gpgprismgr4cycllem7  48091  gpgprismgr4cycllem9  48093  pgnioedg1  48098  pgnioedg2  48099  pgnioedg3  48100  pgnioedg4  48101  pgnioedg5  48102  pgnbgreunbgrlem1  48103  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  pgnbgreunbgrlem2lem3  48106  pgnbgreunbgrlem3  48108  pgnbgreunbgrlem5lem3  48112  pgnbgreunbgrlem5  48113  pgnbgreunbgrlem6  48114  nn0mnd  48167  zlmodzxzel  48343  zlmodzxz0  48344  zlmodzxzscm  48345  zlmodzxzadd  48346  zlmodzxznm  48486  zlmodzxzldeplem  48487  zlmodzxzldeplem2  48490  blen0  48561  nn0sumshdiglemB  48609  fv1arycl  48626  1arympt1  48627  1arympt1fv  48628  1arymaptf1  48631  1arymaptfo  48632  fv2arycl  48637  2arympt  48638  2arymptfv  48639  2arymaptf1  48642  2arymaptfo  48643  ehl2eudisval0  48714  2sphere0  48739  line2ylem  48740  line2  48741  line2x  48743  line2y  48744  ex-gt  49717  ex-gte  49718  aacllem  49790