Theorem c0ex 11210

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

Syntax hints:   ∈ wcel 2106  Vcvv 3474  ℂcc 11110  0cc0 11112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-mulcl 11174  ax-i2m1 11180

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476

This theorem is referenced by:  ofsubeq0  12211  ofsubge0  12213  elnn0  12476  un0mulcl  12508  fcdmnn0supp  12530  fcdmnn0fsupp  12531  fcdmnn0suppg  12532  fcdmnn0fsuppg  12533  nn0ssz  12583  nn0ind-raph  12664  xaddval  13204  xmulval  13206  ser0f  14023  facnn  14237  fac0  14238  bcval  14266  prhash2ex  14361  wrdexb  14477  s1rn  14551  eqs1  14564  repsw1  14735  cshw1  14774  s1co  14786  funcnvs2  14866  funcnvs3  14867  funcnvs4  14868  wrdlen2i  14895  wrd2pr2op  14896  wrd3tpop  14901  wwlktovf1  14910  wrdl3s3  14915  sgnval  15037  iserge0  15609  sum0  15669  sumz  15670  fsumss  15673  fsumser  15678  isumless  15793  geomulcvg  15824  rpnnen2lem1  16159  ruclem4  16179  ruclem8  16182  ruclem11  16185  0bits  16382  gcdval  16439  lcmval  16531  lcmfpr  16566  lcmfunsnlem2  16579  prmreclem2  16852  prmreclem5  16855  vdwapun  16909  smndex1n0mnd  18795  mgmnsgrpex  18814  odval  19404  odf  19407  gexval  19448  telgsumfz0  19862  telgsum  19864  srgbinom  20056  abvtrivd  20452  snifpsrbag  21481  psrbaglesupp  21483  psrbaglesuppOLD  21484  psrbagaddclOLD  21488  psrbaglefi  21491  psrbaglefiOLD  21492  mplcoe5  21601  mplbas2  21603  ltbwe  21605  psrbag0  21629  psrbagev1  21644  psrbagev1OLD  21645  mhpmulcl  21698  cply1coe0bi  21831  m2cpminvid2lem  22263  pmatcollpw3fi1lem1  22295  pmatcollpw3fi1lem2  22296  pmatcollpw3fi1  22297  idpm2idmp  22310  prdsdsf  23880  prdsxmetlem  23881  prdsmet  23883  imasdsf1olem  23886  prdsbl  24007  xrge0gsumle  24356  xrge0tsms  24357  xrhmeo  24469  pcopt  24545  pcopt2  24546  pcoass  24547  rrxcph  24916  rrx0el  24922  rrxbasefi  24934  ovoliunnul  25031  ovolicc1  25040  vitalilem5  25136  mbfpos  25175  0pval  25195  0pledm  25197  i1f1lem  25213  i1f1  25214  itg11  25215  itg1addlem3  25222  itg1addlem4  25223  itg1addlem4OLD  25224  i1fres  25230  itg1climres  25239  mbfi1fseqlem4  25243  mbfi1fseqlem6  25245  mbfi1flimlem  25247  mbfi1flim  25248  xrge0f  25256  itg2ge0  25260  itg2uba  25268  itg2splitlem  25273  itg2monolem1  25275  itg2gt0  25285  itg2cnlem1  25286  ibl0  25311  iblcnlem1  25312  i1fibl  25332  itgeqa  25338  itgcn  25369  dvcmul  25468  dvcmulf  25469  dvexp3  25502  dvef  25504  rolle  25514  dveq0  25524  dv11cn  25525  tdeglem4  25584  tdeglem4OLD  25585  elply2  25717  elplyd  25723  ply1term  25725  ply0  25729  plyeq0  25732  plypf1  25733  plymullem  25737  dgrlt  25787  plymul0or  25801  dvply1  25804  plydivlem4  25816  elqaalem2  25840  iaa  25845  aareccl  25846  aannenlem2  25849  tayl0  25881  taylpfval  25884  dvtaylp  25889  pserdvlem2  25947  abelthlem9  25959  logtayl  26175  cxplogb  26298  leibpilem2  26453  leibpi  26454  jensenlem2  26499  jensen  26500  amgmlem  26501  amgm  26502  igamval  26558  vmaval  26624  vmaf  26630  muval  26643  dchrelbas2  26747  dchrinvcl  26763  dchrptlem2  26775  lgseisenlem4  26888  addsqnreup  26953  pntrlog2bndlem4  27090  pntrlog2bndlem5  27091  padicval  27127  padicabv  27140  ostth1  27143  axlowdimlem8  28245  axlowdimlem9  28246  axlowdimlem10  28247  axlowdimlem11  28248  axlowdimlem12  28249  axlowdimlem13  28250  axlowdimlem17  28254  uspgr1ewop  28543  usgr2v1e2w  28547  umgr2v2eedg  28819  umgr2v2e  28820  umgr2v2evd2  28822  wlkl1loop  28933  2wlklem  28962  usgr2trlncl  29055  2wlkdlem4  29220  2wlkdlem5  29221  2pthdlem1  29222  2wlkdlem10  29227  umgrwwlks2on  29249  rusgrnumwwlkl1  29260  clwwlkn2  29335  0spth  29417  1wlkdlem4  29431  wlk2v2elem1  29446  3wlkdlem4  29453  3wlkdlem5  29454  3pthdlem1  29455  3wlkdlem10  29460  upgr3v3e3cycl  29471  upgr4cycl4dv4e  29476  eulerpathpr  29531  konigsberglem4  29546  konigsberglem5  29547  wlkl0  29658  occllem  30594  0cnfn  31271  0lnfn  31276  nmfn0  31278  nmcexi  31317  nlelchi  31352  fprodex01  32069  s2rn  32148  s3rn  32150  xrge0tsmsd  32250  cyc2fv1  32321  cyc3fv1  32337  cyc3evpm  32350  sgnsval  32361  sgnsf  32362  xrge0iif1  32987  xrge0mulc1cn  32990  gsumesum  33126  esumpfinval  33142  esumpfinvalf  33143  ddeval1  33301  ddeval0  33302  ddemeas  33303  eulerpartlemt  33439  coinfliprv  33550  sgncl  33606  plymul02  33626  plymulx  33628  signsw0glem  33633  signsw0g  33636  signswmnd  33637  signswrid  33638  prodfzo03  33684  circlevma  33723  circlemethhgt  33724  hgt750lemg  33735  hgt750lemb  33737  hgt750lema  33738  hgt750leme  33739  tgoldbachgtde  33741  tgoldbachgt  33744  cvmliftlem4  34348  cvmliftlem5  34349  poimirlem1  36581  poimirlem2  36582  poimirlem3  36583  poimirlem4  36584  poimirlem5  36585  poimirlem6  36586  poimirlem7  36587  poimirlem11  36591  poimirlem12  36592  poimirlem16  36596  poimirlem17  36597  poimirlem19  36599  poimirlem20  36600  poimirlem22  36602  poimirlem23  36603  poimirlem24  36604  poimirlem25  36605  poimirlem28  36608  poimirlem29  36609  poimirlem31  36611  poimirlem32  36612  poimir  36613  broucube  36614  mblfinlem2  36618  mblfinlem3  36619  ismblfin  36621  itg2addnclem  36631  itg2addnclem3  36633  itg2addnc  36634  ftc1anclem3  36655  ftc1anclem5  36657  ftc1anclem7  36659  ftc1anclem8  36660  ftc1anc  36661  dvacos  36665  prdsbnd  36753  heiborlem10  36780  renegclALT  37925  aks4d1p1p4  41028  0prjspnlem  41453  0prjspnrel  41457  diophrw  41585  monotoddzzfi  41769  zindbi  41773  mncn0  41969  aaitgo  41992  flcidc  42004  dfrcl4  42515  fvrcllb0d  42532  fvrcllb0da  42533  iunrelexp0  42541  corclrcl  42546  relexp0idm  42554  dfrtrcl4  42577  corcltrcl  42578  cotrclrcl  42581  ofsubid  43171  lhe4.4ex1a  43176  dvsconst  43177  dvconstbi  43181  binomcxplemnn0  43196  binomcxplemdvbinom  43200  binomcxplemnotnn0  43203  n0p  43818  climrec  44404  limsup10exlem  44573  dvnmptdivc  44739  dvnmul  44744  stoweidlem55  44856  fourierdlem62  44969  fourierdlem104  45011  fouriersw  45032  ovnval2  45346  hoidmvval  45378  tworepnotupword  45685  fun2dmnopgexmpl  46077  el1fzopredsuc  46118  nn0mnd  46674  pzriprnglem4  46893  pzriprnglem5  46894  pzriprnglem7  46896  pzriprnglem9  46898  pzriprnglem10  46899  zlmodzxzel  47116  zlmodzxz0  47117  zlmodzxzscm  47118  zlmodzxzadd  47119  zlmodzxznm  47262  zlmodzxzldeplem  47263  zlmodzxzldeplem2  47266  blen0  47342  nn0sumshdiglemB  47390  fv1arycl  47407  1arympt1  47408  1arympt1fv  47409  1arymaptf1  47412  1arymaptfo  47413  fv2arycl  47418  2arympt  47419  2arymptfv  47420  2arymaptf1  47423  2arymaptfo  47424  ehl2eudisval0  47495  2sphere0  47520  line2ylem  47521  line2  47522  line2x  47524  line2y  47525  ex-gt  47857  ex-gte  47858  aacllem  47932