Theorem c0ex 10978

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

Syntax hints:   ∈ wcel 2107  Vcvv 3433  ℂcc 10878  0cc0 10880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-mulcl 10942  ax-i2m1 10948

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435

This theorem is referenced by:  ofsubeq0  11979  ofsubge0  11981  elnn0  12244  un0mulcl  12276  frnnn0supp  12298  frnnn0fsupp  12299  frnnn0suppg  12300  frnnn0fsuppg  12301  nn0ssz  12350  nn0ind-raph  12429  xaddval  12966  xmulval  12968  ser0f  13785  facnn  13998  fac0  13999  bcval  14027  prhash2ex  14123  wrdexb  14237  s1rn  14313  eqs1  14326  repsw1  14505  cshw1  14544  s1co  14555  funcnvs2  14635  funcnvs3  14636  funcnvs4  14637  wrdlen2i  14664  wrd2pr2op  14665  wrd3tpop  14670  wwlktovf1  14681  wrdl3s3  14686  sgnval  14808  iserge0  15381  sum0  15442  sumz  15443  fsumss  15446  fsumser  15451  isumless  15566  geomulcvg  15597  rpnnen2lem1  15932  ruclem4  15952  ruclem8  15955  ruclem11  15958  0bits  16155  gcdval  16212  lcmval  16306  lcmfpr  16341  lcmfunsnlem2  16354  prmreclem2  16627  prmreclem5  16630  vdwapun  16684  smndex1n0mnd  18560  mgmnsgrpex  18579  odval  19151  odf  19154  gexval  19192  telgsumfz0  19602  telgsum  19604  srgbinom  19790  abvtrivd  20109  snifpsrbag  21134  psrbaglesupp  21136  psrbaglesuppOLD  21137  psrbagaddclOLD  21141  psrbaglefi  21144  psrbaglefiOLD  21145  mplcoe5  21250  mplbas2  21252  ltbwe  21254  psrbag0  21279  psrbagev1  21294  psrbagev1OLD  21295  mhpmulcl  21348  cply1coe0bi  21480  m2cpminvid2lem  21912  pmatcollpw3fi1lem1  21944  pmatcollpw3fi1lem2  21945  pmatcollpw3fi1  21946  idpm2idmp  21959  prdsdsf  23529  prdsxmetlem  23530  prdsmet  23532  imasdsf1olem  23535  prdsbl  23656  xrge0gsumle  24005  xrge0tsms  24006  xrhmeo  24118  pcopt  24194  pcopt2  24195  pcoass  24196  rrxcph  24565  rrx0el  24571  rrxbasefi  24583  ovoliunnul  24680  ovolicc1  24689  vitalilem5  24785  mbfpos  24824  0pval  24844  0pledm  24846  i1f1lem  24862  i1f1  24863  itg11  24864  itg1addlem3  24871  itg1addlem4  24872  itg1addlem4OLD  24873  i1fres  24879  itg1climres  24888  mbfi1fseqlem4  24892  mbfi1fseqlem6  24894  mbfi1flimlem  24896  mbfi1flim  24897  xrge0f  24905  itg2ge0  24909  itg2uba  24917  itg2splitlem  24922  itg2monolem1  24924  itg2gt0  24934  itg2cnlem1  24935  ibl0  24960  iblcnlem1  24961  i1fibl  24981  itgeqa  24987  itgcn  25018  dvcmul  25117  dvcmulf  25118  dvexp3  25151  dvef  25153  rolle  25163  dveq0  25173  dv11cn  25174  tdeglem4  25233  tdeglem4OLD  25234  elply2  25366  elplyd  25372  ply1term  25374  ply0  25378  plyeq0  25381  plypf1  25382  plymullem  25386  dgrlt  25436  plymul0or  25450  dvply1  25453  plydivlem4  25465  elqaalem2  25489  iaa  25494  aareccl  25495  aannenlem2  25498  tayl0  25530  taylpfval  25533  dvtaylp  25538  pserdvlem2  25596  abelthlem9  25608  logtayl  25824  cxplogb  25945  leibpilem2  26100  leibpi  26101  jensenlem2  26146  jensen  26147  amgmlem  26148  amgm  26149  igamval  26205  vmaval  26271  vmaf  26277  muval  26290  dchrelbas2  26394  dchrinvcl  26410  dchrptlem2  26422  lgseisenlem4  26535  addsqnreup  26600  pntrlog2bndlem4  26737  pntrlog2bndlem5  26738  padicval  26774  padicabv  26787  ostth1  26790  axlowdimlem8  27326  axlowdimlem9  27327  axlowdimlem10  27328  axlowdimlem11  27329  axlowdimlem12  27330  axlowdimlem13  27331  axlowdimlem17  27335  uspgr1ewop  27624  usgr2v1e2w  27628  umgr2v2eedg  27900  umgr2v2e  27901  umgr2v2evd2  27903  wlkl1loop  28014  2wlklem  28044  usgr2trlncl  28137  2wlkdlem4  28302  2wlkdlem5  28303  2pthdlem1  28304  2wlkdlem10  28309  umgrwwlks2on  28331  rusgrnumwwlkl1  28342  clwwlkn2  28417  0spth  28499  1wlkdlem4  28513  wlk2v2elem1  28528  3wlkdlem4  28535  3wlkdlem5  28536  3pthdlem1  28537  3wlkdlem10  28542  upgr3v3e3cycl  28553  upgr4cycl4dv4e  28558  eulerpathpr  28613  konigsberglem4  28628  konigsberglem5  28629  wlkl0  28740  occllem  29674  0cnfn  30351  0lnfn  30356  nmfn0  30358  nmcexi  30397  nlelchi  30432  fprodex01  31148  s2rn  31227  s3rn  31229  xrge0tsmsd  31326  cyc2fv1  31397  cyc3fv1  31413  cyc3evpm  31426  sgnsval  31437  sgnsf  31438  xrge0iif1  31897  xrge0mulc1cn  31900  gsumesum  32036  esumpfinval  32052  esumpfinvalf  32053  ddeval1  32211  ddeval0  32212  ddemeas  32213  eulerpartlemt  32347  coinfliprv  32458  sgncl  32514  plymul02  32534  plymulx  32536  signsw0glem  32541  signsw0g  32544  signswmnd  32545  signswrid  32546  prodfzo03  32592  circlevma  32631  circlemethhgt  32632  hgt750lemg  32643  hgt750lemb  32645  hgt750lema  32646  hgt750leme  32647  tgoldbachgtde  32649  tgoldbachgt  32652  cvmliftlem4  33259  cvmliftlem5  33260  poimirlem1  35787  poimirlem2  35788  poimirlem3  35789  poimirlem4  35790  poimirlem5  35791  poimirlem6  35792  poimirlem7  35793  poimirlem11  35797  poimirlem12  35798  poimirlem16  35802  poimirlem17  35803  poimirlem19  35805  poimirlem20  35806  poimirlem22  35808  poimirlem23  35809  poimirlem24  35810  poimirlem25  35811  poimirlem28  35814  poimirlem29  35815  poimirlem31  35817  poimirlem32  35818  poimir  35819  broucube  35820  mblfinlem2  35824  mblfinlem3  35825  ismblfin  35827  itg2addnclem  35837  itg2addnclem3  35839  itg2addnc  35840  ftc1anclem3  35861  ftc1anclem5  35863  ftc1anclem7  35865  ftc1anclem8  35866  ftc1anc  35867  dvacos  35871  prdsbnd  35960  heiborlem10  35987  renegclALT  36984  aks4d1p1p4  40086  evlsbagval  40282  mhphf  40292  0prjspnlem  40467  0prjspnrel  40471  diophrw  40588  monotoddzzfi  40771  zindbi  40775  mncn0  40971  aaitgo  40994  flcidc  41006  dfrcl4  41291  fvrcllb0d  41308  fvrcllb0da  41309  iunrelexp0  41317  corclrcl  41322  relexp0idm  41330  dfrtrcl4  41353  corcltrcl  41354  cotrclrcl  41357  ofsubid  41949  lhe4.4ex1a  41954  dvsconst  41955  dvconstbi  41959  binomcxplemnn0  41974  binomcxplemdvbinom  41978  binomcxplemnotnn0  41981  n0p  42598  climrec  43151  limsup10exlem  43320  dvnmptdivc  43486  dvnmul  43491  stoweidlem55  43603  fourierdlem62  43716  fourierdlem104  43758  fouriersw  43779  ovnval2  44090  hoidmvval  44122  fun2dmnopgexmpl  44787  el1fzopredsuc  44828  nn0mnd  45384  zlmodzxzel  45702  zlmodzxz0  45703  zlmodzxzscm  45704  zlmodzxzadd  45705  zlmodzxznm  45849  zlmodzxzldeplem  45850  zlmodzxzldeplem2  45853  blen0  45929  nn0sumshdiglemB  45977  fv1arycl  45994  1arympt1  45995  1arympt1fv  45996  1arymaptf1  45999  1arymaptfo  46000  fv2arycl  46005  2arympt  46006  2arymptfv  46007  2arymaptf1  46010  2arymaptfo  46011  ehl2eudisval0  46082  2sphere0  46107  line2ylem  46108  line2  46109  line2x  46111  line2y  46112  ex-gt  46441  ex-gte  46442  aacllem  46516  tworepnotupword  46532