Theorem c0ex 11252

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

Syntax hints:   ∈ wcel 2105  Vcvv 3477  ℂcc 11150  0cc0 11152

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-mulcl 11214  ax-i2m1 11220

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479

This theorem is referenced by:  ofsubeq0  12260  ofsubge0  12262  elnn0  12525  un0mulcl  12557  fcdmnn0supp  12580  fcdmnn0fsupp  12581  fcdmnn0suppg  12582  fcdmnn0fsuppg  12583  nn0ssz  12633  nn0ind-raph  12715  xaddval  13261  xmulval  13263  ser0f  14092  facnn  14310  fac0  14311  bcval  14339  prhash2ex  14434  wrdexb  14559  s1rn  14633  eqs1  14646  repsw1  14817  cshw1  14856  s1co  14868  funcnvs2  14948  funcnvs3  14949  funcnvs4  14950  wrdlen2i  14977  wrd2pr2op  14978  wrd3tpop  14983  wwlktovf1  14992  wrdl3s3  14997  sgnval  15123  iserge0  15693  sum0  15753  sumz  15754  fsumss  15757  fsumser  15762  isumless  15877  geomulcvg  15908  rpnnen2lem1  16246  ruclem4  16266  ruclem8  16269  ruclem11  16272  0bits  16472  gcdval  16529  lcmval  16625  lcmfpr  16660  lcmfunsnlem2  16673  prmreclem2  16950  prmreclem5  16953  vdwapun  17007  smndex1n0mnd  18937  mgmnsgrpex  18956  odval  19566  odf  19569  gexval  19610  telgsumfz0  20024  telgsum  20026  srgbinom  20248  abvtrivd  20849  pzriprnglem4  21512  pzriprnglem5  21513  pzriprnglem7  21515  pzriprnglem9  21517  pzriprnglem10  21518  snifpsrbag  21957  psrbaglesupp  21959  psrbaglefi  21963  mplcoe5  22075  mplbas2  22077  ltbwe  22079  psrbag0  22103  psrbagev1  22118  mhpmulcl  22170  psdmplcl  22183  cply1coe0bi  22321  m2cpminvid2lem  22775  pmatcollpw3fi1lem1  22807  pmatcollpw3fi1lem2  22808  pmatcollpw3fi1  22809  idpm2idmp  22822  prdsdsf  24392  prdsxmetlem  24393  prdsmet  24395  imasdsf1olem  24398  prdsbl  24519  xrge0gsumle  24868  xrge0tsms  24869  xrhmeo  24990  pcopt  25068  pcopt2  25069  pcoass  25070  rrxcph  25439  rrx0el  25445  rrxbasefi  25457  ovoliunnul  25555  ovolicc1  25564  vitalilem5  25660  mbfpos  25699  0pval  25719  0pledm  25721  i1f1lem  25737  i1f1  25738  itg11  25739  itg1addlem3  25746  itg1addlem4  25747  itg1addlem4OLD  25748  i1fres  25754  itg1climres  25763  mbfi1fseqlem4  25767  mbfi1fseqlem6  25769  mbfi1flimlem  25771  mbfi1flim  25772  xrge0f  25780  itg2ge0  25784  itg2uba  25792  itg2splitlem  25797  itg2monolem1  25799  itg2gt0  25809  itg2cnlem1  25810  ibl0  25836  iblcnlem1  25837  i1fibl  25857  itgeqa  25863  itgcn  25894  dvcmul  25995  dvcmulf  25996  dvexp3  26030  dvef  26032  rolle  26042  dveq0  26053  dv11cn  26054  tdeglem4  26113  elply2  26249  elplyd  26255  ply1term  26257  ply0  26261  plyeq0  26264  plypf1  26265  plymullem  26269  dgrlt  26320  plymul0or  26336  dvply1  26339  plydivlem4  26352  elqaalem2  26376  iaa  26381  aareccl  26382  aannenlem2  26385  tayl0  26417  taylpfval  26420  dvtaylp  26426  pserdvlem2  26486  abelthlem9  26498  logtayl  26716  cxplogb  26843  leibpilem2  26998  leibpi  26999  jensenlem2  27045  jensen  27046  amgmlem  27047  amgm  27048  igamval  27104  vmaval  27170  vmaf  27176  muval  27189  dchrelbas2  27295  dchrinvcl  27311  dchrptlem2  27323  lgseisenlem4  27436  addsqnreup  27501  pntrlog2bndlem4  27638  pntrlog2bndlem5  27639  padicval  27675  padicabv  27688  ostth1  27691  axlowdimlem8  28978  axlowdimlem9  28979  axlowdimlem10  28980  axlowdimlem11  28981  axlowdimlem12  28982  axlowdimlem13  28983  axlowdimlem17  28987  uspgr1ewop  29279  usgr2v1e2w  29283  umgr2v2eedg  29556  umgr2v2e  29557  umgr2v2evd2  29559  wlkl1loop  29670  2wlklem  29699  usgr2trlncl  29792  2wlkdlem4  29957  2wlkdlem5  29958  2pthdlem1  29959  2wlkdlem10  29964  umgrwwlks2on  29986  rusgrnumwwlkl1  29997  clwwlkn2  30072  0spth  30154  1wlkdlem4  30168  wlk2v2elem1  30183  3wlkdlem4  30190  3wlkdlem5  30191  3pthdlem1  30192  3wlkdlem10  30197  upgr3v3e3cycl  30208  upgr4cycl4dv4e  30213  eulerpathpr  30268  konigsberglem4  30283  konigsberglem5  30284  wlkl0  30395  occllem  31331  0cnfn  32008  0lnfn  32013  nmfn0  32015  nmcexi  32054  nlelchi  32089  fprodex01  32831  s2rnOLD  32912  s3rnOLD  32914  xrge0tsmsd  33047  cyc2fv1  33123  cyc3fv1  33139  cyc3evpm  33152  sgnsval  33163  sgnsf  33164  elrgspnlem1  33231  elrgspnlem4  33234  constr01  33746  constrss  33747  constrconj  33749  xrge0iif1  33898  xrge0mulc1cn  33901  gsumesum  34039  esumpfinval  34055  esumpfinvalf  34056  ddeval1  34214  ddeval0  34215  ddemeas  34216  eulerpartlemt  34352  coinfliprv  34463  sgncl  34519  plymul02  34539  plymulx  34541  signsw0glem  34546  signsw0g  34549  signswmnd  34550  signswrid  34551  prodfzo03  34596  circlevma  34635  circlemethhgt  34636  hgt750lemg  34647  hgt750lemb  34649  hgt750lema  34650  hgt750leme  34651  tgoldbachgtde  34653  tgoldbachgt  34656  cvmliftlem4  35272  cvmliftlem5  35273  poimirlem1  37607  poimirlem2  37608  poimirlem3  37609  poimirlem4  37610  poimirlem5  37611  poimirlem6  37612  poimirlem7  37613  poimirlem11  37617  poimirlem12  37618  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem22  37628  poimirlem23  37629  poimirlem24  37630  poimirlem25  37631  poimirlem28  37634  poimirlem29  37635  poimirlem31  37637  poimirlem32  37638  poimir  37639  broucube  37640  mblfinlem2  37644  mblfinlem3  37645  ismblfin  37647  itg2addnclem  37657  itg2addnclem3  37659  itg2addnc  37660  ftc1anclem3  37681  ftc1anclem5  37683  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  dvacos  37691  prdsbnd  37779  heiborlem10  37806  renegclALT  38944  aks4d1p1p4  42052  aks6d1c7lem1  42161  readvrec  42370  0prjspnlem  42609  0prjspnrel  42613  diophrw  42746  monotoddzzfi  42930  zindbi  42934  mncn0  43127  aaitgo  43150  flcidc  43158  dfrcl4  43665  fvrcllb0d  43682  fvrcllb0da  43683  iunrelexp0  43691  corclrcl  43696  relexp0idm  43704  dfrtrcl4  43727  corcltrcl  43728  cotrclrcl  43731  ofsubid  44319  lhe4.4ex1a  44324  dvsconst  44325  dvconstbi  44329  binomcxplemnn0  44344  binomcxplemdvbinom  44348  binomcxplemnotnn0  44351  n0p  44982  climrec  45558  limsup10exlem  45727  dvnmptdivc  45893  dvnmul  45898  stoweidlem55  46010  fourierdlem62  46123  fourierdlem104  46165  fouriersw  46186  ovnval2  46500  hoidmvval  46532  tworepnotupword  46839  fun2dmnopgexmpl  47233  el1fzopredsuc  47274  stgrusgra  47861  stgr1  47863  stgrnbgr0  47866  isubgr3stgrlem3  47870  isubgr3stgrlem7  47874  usgrexmpl1lem  47915  usgrexmpl1tri  47919  usgrexmpl2lem  47920  usgrexmpl2nb0  47925  usgrexmpl2nb1  47926  usgrexmpl2nb2  47927  usgrexmpl2nb3  47928  usgrexmpl2nb4  47929  usgrexmpl2nb5  47930  usgrexmpl2trifr  47931  gpgedgel  47942  gpgvtx0  47943  gpgedgvtx0  47953  gpgvtxedg0  47955  gpgvtxedg1  47956  gpg5nbgrvtx03starlem1  47958  gpg5nbgrvtx03starlem2  47959  gpg5nbgrvtx03starlem3  47960  gpg5nbgrvtx13starlem1  47961  gpg5nbgrvtx13starlem3  47963  gpg3nbgrvtx0  47966  gpg3nbgrvtx0ALT  47967  gpg3nbgrvtx1  47968  gpgcubic  47969  gpg5nbgr3star  47971  nn0mnd  48022  zlmodzxzel  48199  zlmodzxz0  48200  zlmodzxzscm  48201  zlmodzxzadd  48202  zlmodzxznm  48342  zlmodzxzldeplem  48343  zlmodzxzldeplem2  48346  blen0  48421  nn0sumshdiglemB  48469  fv1arycl  48486  1arympt1  48487  1arympt1fv  48488  1arymaptf1  48491  1arymaptfo  48492  fv2arycl  48497  2arympt  48498  2arymptfv  48499  2arymaptf1  48502  2arymaptfo  48503  ehl2eudisval0  48574  2sphere0  48599  line2ylem  48600  line2  48601  line2x  48603  line2y  48604  ex-gt  48958  ex-gte  48959  aacllem  49031