Theorem c0ex 10624

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

Syntax hints:   ∈ wcel 2111  Vcvv 3441  ℂcc 10524  0cc0 10526

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-mulcl 10588  ax-i2m1 10594

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443

This theorem is referenced by:  ofsubeq0  11622  ofsubge0  11624  elnn0  11887  un0mulcl  11919  frnnn0supp  11941  frnnn0fsupp  11942  nn0ssz  11991  nn0ind-raph  12070  xaddval  12604  xmulval  12606  ser0f  13419  facnn  13631  fac0  13632  bcval  13660  prhash2ex  13756  wrdexb  13868  s1rn  13944  eqs1  13957  repsw1  14136  cshw1  14175  s1co  14186  funcnvs2  14266  funcnvs3  14267  funcnvs4  14268  wrdlen2i  14295  wrd2pr2op  14296  wrd3tpop  14301  wwlktovf1  14312  wrdl3s3  14317  sgnval  14439  iserge0  15009  sum0  15070  sumz  15071  fsumss  15074  fsumser  15079  isumless  15192  geomulcvg  15224  rpnnen2lem1  15559  ruclem4  15579  ruclem8  15582  ruclem11  15585  0bits  15778  gcdval  15835  lcmval  15926  lcmfpr  15961  lcmfunsnlem2  15974  prmreclem2  16243  prmreclem5  16246  vdwapun  16300  smndex1n0mnd  18069  mgmnsgrpex  18088  odval  18654  odf  18657  gexval  18695  telgsumfz0  19105  telgsum  19107  srgbinom  19288  abvtrivd  19604  snifpsrbag  20604  psrbaglesupp  20606  psrbagaddcl  20608  psrbaglefi  20610  mplcoe5  20708  mplbas2  20710  ltbwe  20712  psrbag0  20733  psrbagev1  20749  cply1coe0bi  20929  m2cpminvid2lem  21359  pmatcollpw3fi1lem1  21391  pmatcollpw3fi1lem2  21392  pmatcollpw3fi1  21393  idpm2idmp  21406  prdsdsf  22974  prdsxmetlem  22975  prdsmet  22977  imasdsf1olem  22980  prdsbl  23098  xrge0gsumle  23438  xrge0tsms  23439  xrhmeo  23551  pcopt  23627  pcopt2  23628  pcoass  23629  rrxcph  23996  rrx0el  24002  rrxbasefi  24014  ovoliunnul  24111  ovolicc1  24120  vitalilem5  24216  mbfpos  24255  0pval  24275  0pledm  24277  i1f1lem  24293  i1f1  24294  itg11  24295  itg1addlem3  24302  itg1addlem4  24303  i1fres  24309  itg1climres  24318  mbfi1fseqlem4  24322  mbfi1fseqlem6  24324  mbfi1flimlem  24326  mbfi1flim  24327  xrge0f  24335  itg2ge0  24339  itg2uba  24347  itg2splitlem  24352  itg2monolem1  24354  itg2gt0  24364  itg2cnlem1  24365  ibl0  24390  iblcnlem1  24391  i1fibl  24411  itgeqa  24417  itgcn  24448  dvcmul  24547  dvcmulf  24548  dvexp3  24581  dvef  24583  rolle  24593  dveq0  24603  dv11cn  24604  tdeglem4  24661  elply2  24793  elplyd  24799  ply1term  24801  ply0  24805  plyeq0  24808  plypf1  24809  plymullem  24813  dgrlt  24863  plymul0or  24877  dvply1  24880  plydivlem4  24892  elqaalem2  24916  iaa  24921  aareccl  24922  aannenlem2  24925  tayl0  24957  taylpfval  24960  dvtaylp  24965  pserdvlem2  25023  abelthlem9  25035  logtayl  25251  cxplogb  25372  leibpilem2  25527  leibpi  25528  jensenlem2  25573  jensen  25574  amgmlem  25575  amgm  25576  igamval  25632  vmaval  25698  vmaf  25704  muval  25717  dchrelbas2  25821  dchrinvcl  25837  dchrptlem2  25849  lgseisenlem4  25962  addsqnreup  26027  pntrlog2bndlem4  26164  pntrlog2bndlem5  26165  padicval  26201  padicabv  26214  ostth1  26217  axlowdimlem8  26743  axlowdimlem9  26744  axlowdimlem10  26745  axlowdimlem11  26746  axlowdimlem12  26747  axlowdimlem13  26748  axlowdimlem17  26752  uspgr1ewop  27038  usgr2v1e2w  27042  umgr2v2eedg  27314  umgr2v2e  27315  umgr2v2evd2  27317  wlkl1loop  27427  2wlklem  27457  usgr2trlncl  27549  2wlkdlem4  27714  2wlkdlem5  27715  2pthdlem1  27716  2wlkdlem10  27721  umgrwwlks2on  27743  rusgrnumwwlkl1  27754  clwwlkn2  27829  0spth  27911  1wlkdlem4  27925  wlk2v2elem1  27940  3wlkdlem4  27947  3wlkdlem5  27948  3pthdlem1  27949  3wlkdlem10  27954  upgr3v3e3cycl  27965  upgr4cycl4dv4e  27970  eulerpathpr  28025  konigsberglem4  28040  konigsberglem5  28041  wlkl0  28152  occllem  29086  0cnfn  29763  0lnfn  29768  nmfn0  29770  nmcexi  29809  nlelchi  29844  fprodex01  30567  s2rn  30646  s3rn  30648  xrge0tsmsd  30742  cyc2fv1  30813  cyc3fv1  30829  cyc3evpm  30842  sgnsval  30853  sgnsf  30854  xrge0iif1  31291  xrge0mulc1cn  31294  gsumesum  31428  esumpfinval  31444  esumpfinvalf  31445  ddeval1  31603  ddeval0  31604  ddemeas  31605  eulerpartlemt  31739  coinfliprv  31850  sgncl  31906  plymul02  31926  plymulx  31928  signsw0glem  31933  signsw0g  31936  signswmnd  31937  signswrid  31938  prodfzo03  31984  circlevma  32023  circlemethhgt  32024  hgt750lemg  32035  hgt750lemb  32037  hgt750lema  32038  hgt750leme  32039  tgoldbachgtde  32041  tgoldbachgt  32044  cvmliftlem4  32648  cvmliftlem5  32649  poimirlem1  35058  poimirlem2  35059  poimirlem3  35060  poimirlem4  35061  poimirlem5  35062  poimirlem6  35063  poimirlem7  35064  poimirlem11  35068  poimirlem12  35069  poimirlem16  35073  poimirlem17  35074  poimirlem19  35076  poimirlem20  35077  poimirlem22  35079  poimirlem23  35080  poimirlem24  35081  poimirlem25  35082  poimirlem28  35085  poimirlem29  35086  poimirlem31  35088  poimirlem32  35089  poimir  35090  broucube  35091  mblfinlem2  35095  mblfinlem3  35096  ismblfin  35098  itg2addnclem  35108  itg2addnclem3  35110  itg2addnc  35111  ftc1anclem3  35132  ftc1anclem5  35134  ftc1anclem7  35136  ftc1anclem8  35137  ftc1anc  35138  dvacos  35142  prdsbnd  35231  heiborlem10  35258  renegclALT  36259  0prjspnlem  39612  0prjspnrel  39613  diophrw  39700  monotoddzzfi  39883  zindbi  39887  mncn0  40083  aaitgo  40106  flcidc  40118  dfrcl4  40377  fvrcllb0d  40394  fvrcllb0da  40395  iunrelexp0  40403  corclrcl  40408  relexp0idm  40416  dfrtrcl4  40439  corcltrcl  40440  cotrclrcl  40443  ofsubid  41028  lhe4.4ex1a  41033  dvsconst  41034  dvconstbi  41038  binomcxplemnn0  41053  binomcxplemdvbinom  41057  binomcxplemnotnn0  41060  n0p  41677  climrec  42245  limsup10exlem  42414  dvnmptdivc  42580  dvnmul  42585  stoweidlem55  42697  fourierdlem62  42810  fourierdlem104  42852  fouriersw  42873  ovnval2  43184  hoidmvval  43216  fun2dmnopgexmpl  43840  el1fzopredsuc  43882  nn0mnd  44439  zlmodzxzel  44757  zlmodzxz0  44758  zlmodzxzscm  44759  zlmodzxzadd  44760  zlmodzxznm  44906  zlmodzxzldeplem  44907  zlmodzxzldeplem2  44910  blen0  44986  nn0sumshdiglemB  45034  fv1arycl  45051  1arympt1  45052  1arympt1fv  45053  1arymaptf1  45056  1arymaptfo  45057  fv2arycl  45062  2arympt  45063  2arymptfv  45064  2arymaptf1  45067  2arymaptfo  45068  ehl2eudisval0  45139  2sphere0  45164  line2ylem  45165  line2  45166  line2x  45168  line2y  45169  ex-gt  45254  ex-gte  45255  aacllem  45329