Theorem c0ex 11232

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

Syntax hints:   ∈ wcel 2099  Vcvv 3470  ℂcc 11130  0cc0 11132

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-1cn 11190  ax-icn 11191  ax-addcl 11192  ax-mulcl 11194  ax-i2m1 11200

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3472

This theorem is referenced by:  ofsubeq0  12233  ofsubge0  12235  elnn0  12498  un0mulcl  12530  fcdmnn0supp  12552  fcdmnn0fsupp  12553  fcdmnn0suppg  12554  fcdmnn0fsuppg  12555  nn0ssz  12605  nn0ind-raph  12686  xaddval  13228  xmulval  13230  ser0f  14046  facnn  14260  fac0  14261  bcval  14289  prhash2ex  14384  wrdexb  14501  s1rn  14575  eqs1  14588  repsw1  14759  cshw1  14798  s1co  14810  funcnvs2  14890  funcnvs3  14891  funcnvs4  14892  wrdlen2i  14919  wrd2pr2op  14920  wrd3tpop  14925  wwlktovf1  14934  wrdl3s3  14939  sgnval  15061  iserge0  15633  sum0  15693  sumz  15694  fsumss  15697  fsumser  15702  isumless  15817  geomulcvg  15848  rpnnen2lem1  16184  ruclem4  16204  ruclem8  16207  ruclem11  16210  0bits  16407  gcdval  16464  lcmval  16556  lcmfpr  16591  lcmfunsnlem2  16604  prmreclem2  16879  prmreclem5  16882  vdwapun  16936  smndex1n0mnd  18857  mgmnsgrpex  18876  odval  19482  odf  19485  gexval  19526  telgsumfz0  19940  telgsum  19942  srgbinom  20164  abvtrivd  20713  pzriprnglem4  21403  pzriprnglem5  21404  pzriprnglem7  21406  pzriprnglem9  21408  pzriprnglem10  21409  snifpsrbag  21848  psrbaglesupp  21850  psrbaglesuppOLD  21851  psrbagaddclOLD  21855  psrbaglefi  21858  psrbaglefiOLD  21859  mplcoe5  21971  mplbas2  21973  ltbwe  21975  psrbag0  21999  psrbagev1  22014  psrbagev1OLD  22015  mhpmulcl  22066  psdmplcl  22079  cply1coe0bi  22214  m2cpminvid2lem  22649  pmatcollpw3fi1lem1  22681  pmatcollpw3fi1lem2  22682  pmatcollpw3fi1  22683  idpm2idmp  22696  prdsdsf  24266  prdsxmetlem  24267  prdsmet  24269  imasdsf1olem  24272  prdsbl  24393  xrge0gsumle  24742  xrge0tsms  24743  xrhmeo  24864  pcopt  24942  pcopt2  24943  pcoass  24944  rrxcph  25313  rrx0el  25319  rrxbasefi  25331  ovoliunnul  25429  ovolicc1  25438  vitalilem5  25534  mbfpos  25573  0pval  25593  0pledm  25595  i1f1lem  25611  i1f1  25612  itg11  25613  itg1addlem3  25620  itg1addlem4  25621  itg1addlem4OLD  25622  i1fres  25628  itg1climres  25637  mbfi1fseqlem4  25641  mbfi1fseqlem6  25643  mbfi1flimlem  25645  mbfi1flim  25646  xrge0f  25654  itg2ge0  25658  itg2uba  25666  itg2splitlem  25671  itg2monolem1  25673  itg2gt0  25683  itg2cnlem1  25684  ibl0  25709  iblcnlem1  25710  i1fibl  25730  itgeqa  25736  itgcn  25767  dvcmul  25868  dvcmulf  25869  dvexp3  25903  dvef  25905  rolle  25915  dveq0  25926  dv11cn  25927  tdeglem4  25988  tdeglem4OLD  25989  elply2  26123  elplyd  26129  ply1term  26131  ply0  26135  plyeq0  26138  plypf1  26139  plymullem  26143  dgrlt  26194  plymul0or  26208  dvply1  26211  plydivlem4  26224  elqaalem2  26248  iaa  26253  aareccl  26254  aannenlem2  26257  tayl0  26289  taylpfval  26292  dvtaylp  26298  pserdvlem2  26358  abelthlem9  26370  logtayl  26587  cxplogb  26711  leibpilem2  26866  leibpi  26867  jensenlem2  26913  jensen  26914  amgmlem  26915  amgm  26916  igamval  26972  vmaval  27038  vmaf  27044  muval  27057  dchrelbas2  27163  dchrinvcl  27179  dchrptlem2  27191  lgseisenlem4  27304  addsqnreup  27369  pntrlog2bndlem4  27506  pntrlog2bndlem5  27507  padicval  27543  padicabv  27556  ostth1  27559  axlowdimlem8  28753  axlowdimlem9  28754  axlowdimlem10  28755  axlowdimlem11  28756  axlowdimlem12  28757  axlowdimlem13  28758  axlowdimlem17  28762  uspgr1ewop  29054  usgr2v1e2w  29058  umgr2v2eedg  29331  umgr2v2e  29332  umgr2v2evd2  29334  wlkl1loop  29445  2wlklem  29474  usgr2trlncl  29567  2wlkdlem4  29732  2wlkdlem5  29733  2pthdlem1  29734  2wlkdlem10  29739  umgrwwlks2on  29761  rusgrnumwwlkl1  29772  clwwlkn2  29847  0spth  29929  1wlkdlem4  29943  wlk2v2elem1  29958  3wlkdlem4  29965  3wlkdlem5  29966  3pthdlem1  29967  3wlkdlem10  29972  upgr3v3e3cycl  29983  upgr4cycl4dv4e  29988  eulerpathpr  30043  konigsberglem4  30058  konigsberglem5  30059  wlkl0  30170  occllem  31106  0cnfn  31783  0lnfn  31788  nmfn0  31790  nmcexi  31829  nlelchi  31864  fprodex01  32582  s2rn  32661  s3rn  32663  xrge0tsmsd  32765  cyc2fv1  32836  cyc3fv1  32852  cyc3evpm  32865  sgnsval  32876  sgnsf  32877  xrge0iif1  33533  xrge0mulc1cn  33536  gsumesum  33672  esumpfinval  33688  esumpfinvalf  33689  ddeval1  33847  ddeval0  33848  ddemeas  33849  eulerpartlemt  33985  coinfliprv  34096  sgncl  34152  plymul02  34172  plymulx  34174  signsw0glem  34179  signsw0g  34182  signswmnd  34183  signswrid  34184  prodfzo03  34229  circlevma  34268  circlemethhgt  34269  hgt750lemg  34280  hgt750lemb  34282  hgt750lema  34283  hgt750leme  34284  tgoldbachgtde  34286  tgoldbachgt  34289  cvmliftlem4  34892  cvmliftlem5  34893  poimirlem1  37088  poimirlem2  37089  poimirlem3  37090  poimirlem4  37091  poimirlem5  37092  poimirlem6  37093  poimirlem7  37094  poimirlem11  37098  poimirlem12  37099  poimirlem16  37103  poimirlem17  37104  poimirlem19  37106  poimirlem20  37107  poimirlem22  37109  poimirlem23  37110  poimirlem24  37111  poimirlem25  37112  poimirlem28  37115  poimirlem29  37116  poimirlem31  37118  poimirlem32  37119  poimir  37120  broucube  37121  mblfinlem2  37125  mblfinlem3  37126  ismblfin  37128  itg2addnclem  37138  itg2addnclem3  37140  itg2addnc  37141  ftc1anclem3  37162  ftc1anclem5  37164  ftc1anclem7  37166  ftc1anclem8  37167  ftc1anc  37168  dvacos  37172  prdsbnd  37260  heiborlem10  37287  renegclALT  38429  aks4d1p1p4  41536  aks6d1c7lem1  41646  0prjspnlem  42041  0prjspnrel  42045  diophrw  42173  monotoddzzfi  42357  zindbi  42361  mncn0  42557  aaitgo  42580  flcidc  42592  dfrcl4  43100  fvrcllb0d  43117  fvrcllb0da  43118  iunrelexp0  43126  corclrcl  43131  relexp0idm  43139  dfrtrcl4  43162  corcltrcl  43163  cotrclrcl  43166  ofsubid  43755  lhe4.4ex1a  43760  dvsconst  43761  dvconstbi  43765  binomcxplemnn0  43780  binomcxplemdvbinom  43784  binomcxplemnotnn0  43787  n0p  44401  climrec  44985  limsup10exlem  45154  dvnmptdivc  45320  dvnmul  45325  stoweidlem55  45437  fourierdlem62  45550  fourierdlem104  45592  fouriersw  45613  ovnval2  45927  hoidmvval  45959  tworepnotupword  46266  fun2dmnopgexmpl  46658  el1fzopredsuc  46699  nn0mnd  47235  zlmodzxzel  47413  zlmodzxz0  47414  zlmodzxzscm  47415  zlmodzxzadd  47416  zlmodzxznm  47559  zlmodzxzldeplem  47560  zlmodzxzldeplem2  47563  blen0  47639  nn0sumshdiglemB  47687  fv1arycl  47704  1arympt1  47705  1arympt1fv  47706  1arymaptf1  47709  1arymaptfo  47710  fv2arycl  47715  2arympt  47716  2arymptfv  47717  2arymaptf1  47720  2arymaptfo  47721  ehl2eudisval0  47792  2sphere0  47817  line2ylem  47818  line2  47819  line2x  47821  line2y  47822  ex-gt  48153  ex-gte  48154  aacllem  48228