Theorem c0ex 10900

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

Syntax hints:   ∈ wcel 2108  Vcvv 3422  ℂcc 10800  0cc0 10802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-mulcl 10864  ax-i2m1 10870

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424

This theorem is referenced by:  ofsubeq0  11900  ofsubge0  11902  elnn0  12165  un0mulcl  12197  frnnn0supp  12219  frnnn0fsupp  12220  frnnn0suppg  12221  frnnn0fsuppg  12222  nn0ssz  12271  nn0ind-raph  12350  xaddval  12886  xmulval  12888  ser0f  13704  facnn  13917  fac0  13918  bcval  13946  prhash2ex  14042  wrdexb  14156  s1rn  14232  eqs1  14245  repsw1  14424  cshw1  14463  s1co  14474  funcnvs2  14554  funcnvs3  14555  funcnvs4  14556  wrdlen2i  14583  wrd2pr2op  14584  wrd3tpop  14589  wwlktovf1  14600  wrdl3s3  14605  sgnval  14727  iserge0  15300  sum0  15361  sumz  15362  fsumss  15365  fsumser  15370  isumless  15485  geomulcvg  15516  rpnnen2lem1  15851  ruclem4  15871  ruclem8  15874  ruclem11  15877  0bits  16074  gcdval  16131  lcmval  16225  lcmfpr  16260  lcmfunsnlem2  16273  prmreclem2  16546  prmreclem5  16549  vdwapun  16603  smndex1n0mnd  18466  mgmnsgrpex  18485  odval  19057  odf  19060  gexval  19098  telgsumfz0  19508  telgsum  19510  srgbinom  19696  abvtrivd  20015  snifpsrbag  21035  psrbaglesupp  21037  psrbaglesuppOLD  21038  psrbagaddclOLD  21042  psrbaglefi  21045  psrbaglefiOLD  21046  mplcoe5  21151  mplbas2  21153  ltbwe  21155  psrbag0  21180  psrbagev1  21195  psrbagev1OLD  21196  mhpmulcl  21249  cply1coe0bi  21381  m2cpminvid2lem  21811  pmatcollpw3fi1lem1  21843  pmatcollpw3fi1lem2  21844  pmatcollpw3fi1  21845  idpm2idmp  21858  prdsdsf  23428  prdsxmetlem  23429  prdsmet  23431  imasdsf1olem  23434  prdsbl  23553  xrge0gsumle  23902  xrge0tsms  23903  xrhmeo  24015  pcopt  24091  pcopt2  24092  pcoass  24093  rrxcph  24461  rrx0el  24467  rrxbasefi  24479  ovoliunnul  24576  ovolicc1  24585  vitalilem5  24681  mbfpos  24720  0pval  24740  0pledm  24742  i1f1lem  24758  i1f1  24759  itg11  24760  itg1addlem3  24767  itg1addlem4  24768  itg1addlem4OLD  24769  i1fres  24775  itg1climres  24784  mbfi1fseqlem4  24788  mbfi1fseqlem6  24790  mbfi1flimlem  24792  mbfi1flim  24793  xrge0f  24801  itg2ge0  24805  itg2uba  24813  itg2splitlem  24818  itg2monolem1  24820  itg2gt0  24830  itg2cnlem1  24831  ibl0  24856  iblcnlem1  24857  i1fibl  24877  itgeqa  24883  itgcn  24914  dvcmul  25013  dvcmulf  25014  dvexp3  25047  dvef  25049  rolle  25059  dveq0  25069  dv11cn  25070  tdeglem4  25129  tdeglem4OLD  25130  elply2  25262  elplyd  25268  ply1term  25270  ply0  25274  plyeq0  25277  plypf1  25278  plymullem  25282  dgrlt  25332  plymul0or  25346  dvply1  25349  plydivlem4  25361  elqaalem2  25385  iaa  25390  aareccl  25391  aannenlem2  25394  tayl0  25426  taylpfval  25429  dvtaylp  25434  pserdvlem2  25492  abelthlem9  25504  logtayl  25720  cxplogb  25841  leibpilem2  25996  leibpi  25997  jensenlem2  26042  jensen  26043  amgmlem  26044  amgm  26045  igamval  26101  vmaval  26167  vmaf  26173  muval  26186  dchrelbas2  26290  dchrinvcl  26306  dchrptlem2  26318  lgseisenlem4  26431  addsqnreup  26496  pntrlog2bndlem4  26633  pntrlog2bndlem5  26634  padicval  26670  padicabv  26683  ostth1  26686  axlowdimlem8  27220  axlowdimlem9  27221  axlowdimlem10  27222  axlowdimlem11  27223  axlowdimlem12  27224  axlowdimlem13  27225  axlowdimlem17  27229  uspgr1ewop  27518  usgr2v1e2w  27522  umgr2v2eedg  27794  umgr2v2e  27795  umgr2v2evd2  27797  wlkl1loop  27907  2wlklem  27937  usgr2trlncl  28029  2wlkdlem4  28194  2wlkdlem5  28195  2pthdlem1  28196  2wlkdlem10  28201  umgrwwlks2on  28223  rusgrnumwwlkl1  28234  clwwlkn2  28309  0spth  28391  1wlkdlem4  28405  wlk2v2elem1  28420  3wlkdlem4  28427  3wlkdlem5  28428  3pthdlem1  28429  3wlkdlem10  28434  upgr3v3e3cycl  28445  upgr4cycl4dv4e  28450  eulerpathpr  28505  konigsberglem4  28520  konigsberglem5  28521  wlkl0  28632  occllem  29566  0cnfn  30243  0lnfn  30248  nmfn0  30250  nmcexi  30289  nlelchi  30324  fprodex01  31041  s2rn  31120  s3rn  31122  xrge0tsmsd  31219  cyc2fv1  31290  cyc3fv1  31306  cyc3evpm  31319  sgnsval  31330  sgnsf  31331  xrge0iif1  31790  xrge0mulc1cn  31793  gsumesum  31927  esumpfinval  31943  esumpfinvalf  31944  ddeval1  32102  ddeval0  32103  ddemeas  32104  eulerpartlemt  32238  coinfliprv  32349  sgncl  32405  plymul02  32425  plymulx  32427  signsw0glem  32432  signsw0g  32435  signswmnd  32436  signswrid  32437  prodfzo03  32483  circlevma  32522  circlemethhgt  32523  hgt750lemg  32534  hgt750lemb  32536  hgt750lema  32537  hgt750leme  32538  tgoldbachgtde  32540  tgoldbachgt  32543  cvmliftlem4  33150  cvmliftlem5  33151  poimirlem1  35705  poimirlem2  35706  poimirlem3  35707  poimirlem4  35708  poimirlem5  35709  poimirlem6  35710  poimirlem7  35711  poimirlem11  35715  poimirlem12  35716  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem22  35726  poimirlem23  35727  poimirlem24  35728  poimirlem25  35729  poimirlem28  35732  poimirlem29  35733  poimirlem31  35735  poimirlem32  35736  poimir  35737  broucube  35738  mblfinlem2  35742  mblfinlem3  35743  ismblfin  35745  itg2addnclem  35755  itg2addnclem3  35757  itg2addnc  35758  ftc1anclem3  35779  ftc1anclem5  35781  ftc1anclem7  35783  ftc1anclem8  35784  ftc1anc  35785  dvacos  35789  prdsbnd  35878  heiborlem10  35905  renegclALT  36904  aks4d1p1p4  40007  evlsbagval  40198  mhphf  40208  0prjspnlem  40381  0prjspnrel  40385  diophrw  40497  monotoddzzfi  40680  zindbi  40684  mncn0  40880  aaitgo  40903  flcidc  40915  dfrcl4  41173  fvrcllb0d  41190  fvrcllb0da  41191  iunrelexp0  41199  corclrcl  41204  relexp0idm  41212  dfrtrcl4  41235  corcltrcl  41236  cotrclrcl  41239  ofsubid  41831  lhe4.4ex1a  41836  dvsconst  41837  dvconstbi  41841  binomcxplemnn0  41856  binomcxplemdvbinom  41860  binomcxplemnotnn0  41863  n0p  42480  climrec  43034  limsup10exlem  43203  dvnmptdivc  43369  dvnmul  43374  stoweidlem55  43486  fourierdlem62  43599  fourierdlem104  43641  fouriersw  43662  ovnval2  43973  hoidmvval  44005  fun2dmnopgexmpl  44663  el1fzopredsuc  44705  nn0mnd  45261  zlmodzxzel  45579  zlmodzxz0  45580  zlmodzxzscm  45581  zlmodzxzadd  45582  zlmodzxznm  45726  zlmodzxzldeplem  45727  zlmodzxzldeplem2  45730  blen0  45806  nn0sumshdiglemB  45854  fv1arycl  45871  1arympt1  45872  1arympt1fv  45873  1arymaptf1  45876  1arymaptfo  45877  fv2arycl  45882  2arympt  45883  2arymptfv  45884  2arymaptf1  45887  2arymaptfo  45888  ehl2eudisval0  45959  2sphere0  45984  line2ylem  45985  line2  45986  line2x  45988  line2y  45989  ex-gt  46316  ex-gte  46317  aacllem  46391