Theorem c0ex 10635

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

Syntax hints:   ∈ wcel 2114  Vcvv 3494  ℂcc 10535  0cc0 10537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-mulcl 10599  ax-i2m1 10605

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-v 3496

This theorem is referenced by:  ofsubeq0  11635  ofsubge0  11637  elnn0  11900  un0mulcl  11932  frnnn0supp  11954  frnnn0fsupp  11955  nn0ssz  12004  nn0ind-raph  12083  xaddval  12617  xmulval  12619  ser0f  13424  facnn  13636  fac0  13637  bcval  13665  prhash2ex  13761  wrdexb  13874  s1rn  13953  eqs1  13966  repsw1  14145  cshw1  14184  s1co  14195  funcnvs2  14275  funcnvs3  14276  funcnvs4  14277  wrdlen2i  14304  wrd2pr2op  14305  wrd3tpop  14310  wwlktovf1  14321  wrdl3s3  14326  sgnval  14447  iserge0  15017  sum0  15078  sumz  15079  fsumss  15082  fsumser  15087  isumless  15200  geomulcvg  15232  rpnnen2lem1  15567  ruclem4  15587  ruclem8  15590  ruclem11  15593  0bits  15788  gcdval  15845  lcmval  15936  lcmfpr  15971  lcmfunsnlem2  15984  prmreclem2  16253  prmreclem5  16256  vdwapun  16310  smndex1n0mnd  18077  mgmnsgrpex  18096  odval  18662  odf  18665  gexval  18703  telgsumfz0  19112  telgsum  19114  srgbinom  19295  abvtrivd  19611  snifpsrbag  20146  psrbaglesupp  20148  psrbagaddcl  20150  psrbaglefi  20152  mplcoe5  20249  mplbas2  20251  ltbwe  20253  psrbag0  20274  psrbagev1  20290  cply1coe0bi  20468  m2cpminvid2lem  21362  pmatcollpw3fi1lem1  21394  pmatcollpw3fi1lem2  21395  pmatcollpw3fi1  21396  idpm2idmp  21409  prdsdsf  22977  prdsxmetlem  22978  prdsmet  22980  imasdsf1olem  22983  prdsbl  23101  xrge0gsumle  23441  xrge0tsms  23442  xrhmeo  23550  pcopt  23626  pcopt2  23627  pcoass  23628  rrxcph  23995  rrx0el  24001  rrxbasefi  24013  ovoliunnul  24108  ovolicc1  24117  vitalilem5  24213  mbfpos  24252  0pval  24272  0pledm  24274  i1f1lem  24290  i1f1  24291  itg11  24292  itg1addlem3  24299  itg1addlem4  24300  i1fres  24306  itg1climres  24315  mbfi1fseqlem4  24319  mbfi1fseqlem6  24321  mbfi1flimlem  24323  mbfi1flim  24324  xrge0f  24332  itg2ge0  24336  itg2uba  24344  itg2splitlem  24349  itg2monolem1  24351  itg2gt0  24361  itg2cnlem1  24362  ibl0  24387  iblcnlem1  24388  i1fibl  24408  itgeqa  24414  itgcn  24443  dvcmul  24541  dvcmulf  24542  dvexp3  24575  dvef  24577  rolle  24587  dveq0  24597  dv11cn  24598  tdeglem4  24654  elply2  24786  elplyd  24792  ply1term  24794  ply0  24798  plyeq0  24801  plypf1  24802  plymullem  24806  dgrlt  24856  plymul0or  24870  dvply1  24873  plydivlem4  24885  elqaalem2  24909  iaa  24914  aareccl  24915  aannenlem2  24918  tayl0  24950  taylpfval  24953  dvtaylp  24958  pserdvlem2  25016  abelthlem9  25028  logtayl  25243  cxplogb  25364  leibpilem2  25519  leibpi  25520  jensenlem2  25565  jensen  25566  amgmlem  25567  amgm  25568  igamval  25624  vmaval  25690  vmaf  25696  muval  25709  dchrelbas2  25813  dchrinvcl  25829  dchrptlem2  25841  lgseisenlem4  25954  addsqnreup  26019  pntrlog2bndlem4  26156  pntrlog2bndlem5  26157  padicval  26193  padicabv  26206  ostth1  26209  axlowdimlem8  26735  axlowdimlem9  26736  axlowdimlem10  26737  axlowdimlem11  26738  axlowdimlem12  26739  axlowdimlem13  26740  axlowdimlem17  26744  uspgr1ewop  27030  usgr2v1e2w  27034  umgr2v2eedg  27306  umgr2v2e  27307  umgr2v2evd2  27309  wlkl1loop  27419  2wlklem  27449  usgr2trlncl  27541  2wlkdlem4  27707  2wlkdlem5  27708  2pthdlem1  27709  2wlkdlem10  27714  umgrwwlks2on  27736  rusgrnumwwlkl1  27747  clwwlkn2  27822  0spth  27905  1wlkdlem4  27919  wlk2v2elem1  27934  3wlkdlem4  27941  3wlkdlem5  27942  3pthdlem1  27943  3wlkdlem10  27948  upgr3v3e3cycl  27959  upgr4cycl4dv4e  27964  eulerpathpr  28019  konigsberglem4  28034  konigsberglem5  28035  wlkl0  28146  occllem  29080  0cnfn  29757  0lnfn  29762  nmfn0  29764  nmcexi  29803  nlelchi  29838  fprodex01  30541  s2rn  30620  s3rn  30622  xrge0tsmsd  30692  cyc2fv1  30763  cyc3fv1  30779  cyc3evpm  30792  sgnsval  30803  sgnsf  30804  xrge0iif1  31181  xrge0mulc1cn  31184  gsumesum  31318  esumpfinval  31334  esumpfinvalf  31335  ddeval1  31493  ddeval0  31494  ddemeas  31495  eulerpartlemt  31629  coinfliprv  31740  sgncl  31796  plymul02  31816  plymulx  31818  signsw0glem  31823  signsw0g  31826  signswmnd  31827  signswrid  31828  prodfzo03  31874  circlevma  31913  circlemethhgt  31914  hgt750lemg  31925  hgt750lemb  31927  hgt750lema  31928  hgt750leme  31929  tgoldbachgtde  31931  tgoldbachgt  31934  cvmliftlem4  32535  cvmliftlem5  32536  poimirlem1  34908  poimirlem2  34909  poimirlem3  34910  poimirlem4  34911  poimirlem5  34912  poimirlem6  34913  poimirlem7  34914  poimirlem11  34918  poimirlem12  34919  poimirlem16  34923  poimirlem17  34924  poimirlem19  34926  poimirlem20  34927  poimirlem22  34929  poimirlem23  34930  poimirlem24  34931  poimirlem25  34932  poimirlem28  34935  poimirlem29  34936  poimirlem31  34938  poimirlem32  34939  poimir  34940  broucube  34941  mblfinlem2  34945  mblfinlem3  34946  ismblfin  34948  itg2addnclem  34958  itg2addnclem3  34960  itg2addnc  34961  ftc1anclem3  34984  ftc1anclem5  34986  ftc1anclem7  34988  ftc1anclem8  34989  ftc1anc  34990  dvacos  34994  prdsbnd  35086  heiborlem10  35113  renegclALT  36114  0prjspnlem  39317  0prjspnrel  39318  diophrw  39405  monotoddzzfi  39588  zindbi  39592  mncn0  39788  aaitgo  39811  flcidc  39823  dfrcl4  40070  fvrcllb0d  40087  fvrcllb0da  40088  iunrelexp0  40096  corclrcl  40101  relexp0idm  40109  dfrtrcl4  40132  corcltrcl  40133  cotrclrcl  40136  ofsubid  40705  lhe4.4ex1a  40710  dvsconst  40711  dvconstbi  40715  binomcxplemnn0  40730  binomcxplemdvbinom  40734  binomcxplemnotnn0  40737  n0p  41354  climrec  41933  limsup10exlem  42102  dvnmptdivc  42272  dvnmul  42277  stoweidlem55  42389  fourierdlem62  42502  fourierdlem104  42544  fouriersw  42565  ovnval2  42876  hoidmvval  42908  fun2dmnopgexmpl  43532  el1fzopredsuc  43574  nn0mnd  44135  zlmodzxzel  44452  zlmodzxz0  44453  zlmodzxzscm  44454  zlmodzxzadd  44455  zlmodzxznm  44601  zlmodzxzldeplem  44602  zlmodzxzldeplem2  44605  blen0  44681  nn0sumshdiglemB  44729  ehl2eudisval0  44761  2sphere0  44786  line2ylem  44787  line2  44788  line2x  44790  line2y  44791  ex-gt  44876  ex-gte  44877  aacllem  44951