Theorem c0ex 11205

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

Syntax hints:   ∈ wcel 2107  Vcvv 3475  ℂcc 11105  0cc0 11107

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 2704  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-mulcl 11169  ax-i2m1 11175

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477

This theorem is referenced by:  ofsubeq0  12206  ofsubge0  12208  elnn0  12471  un0mulcl  12503  fcdmnn0supp  12525  fcdmnn0fsupp  12526  fcdmnn0suppg  12527  fcdmnn0fsuppg  12528  nn0ssz  12578  nn0ind-raph  12659  xaddval  13199  xmulval  13201  ser0f  14018  facnn  14232  fac0  14233  bcval  14261  prhash2ex  14356  wrdexb  14472  s1rn  14546  eqs1  14559  repsw1  14730  cshw1  14769  s1co  14781  funcnvs2  14861  funcnvs3  14862  funcnvs4  14863  wrdlen2i  14890  wrd2pr2op  14891  wrd3tpop  14896  wwlktovf1  14905  wrdl3s3  14910  sgnval  15032  iserge0  15604  sum0  15664  sumz  15665  fsumss  15668  fsumser  15673  isumless  15788  geomulcvg  15819  rpnnen2lem1  16154  ruclem4  16174  ruclem8  16177  ruclem11  16180  0bits  16377  gcdval  16434  lcmval  16526  lcmfpr  16561  lcmfunsnlem2  16574  prmreclem2  16847  prmreclem5  16850  vdwapun  16904  smndex1n0mnd  18790  mgmnsgrpex  18809  odval  19397  odf  19400  gexval  19441  telgsumfz0  19855  telgsum  19857  srgbinom  20048  abvtrivd  20441  snifpsrbag  21467  psrbaglesupp  21469  psrbaglesuppOLD  21470  psrbagaddclOLD  21474  psrbaglefi  21477  psrbaglefiOLD  21478  mplcoe5  21587  mplbas2  21589  ltbwe  21591  psrbag0  21615  psrbagev1  21630  psrbagev1OLD  21631  mhpmulcl  21684  cply1coe0bi  21816  m2cpminvid2lem  22248  pmatcollpw3fi1lem1  22280  pmatcollpw3fi1lem2  22281  pmatcollpw3fi1  22282  idpm2idmp  22295  prdsdsf  23865  prdsxmetlem  23866  prdsmet  23868  imasdsf1olem  23871  prdsbl  23992  xrge0gsumle  24341  xrge0tsms  24342  xrhmeo  24454  pcopt  24530  pcopt2  24531  pcoass  24532  rrxcph  24901  rrx0el  24907  rrxbasefi  24919  ovoliunnul  25016  ovolicc1  25025  vitalilem5  25121  mbfpos  25160  0pval  25180  0pledm  25182  i1f1lem  25198  i1f1  25199  itg11  25200  itg1addlem3  25207  itg1addlem4  25208  itg1addlem4OLD  25209  i1fres  25215  itg1climres  25224  mbfi1fseqlem4  25228  mbfi1fseqlem6  25230  mbfi1flimlem  25232  mbfi1flim  25233  xrge0f  25241  itg2ge0  25245  itg2uba  25253  itg2splitlem  25258  itg2monolem1  25260  itg2gt0  25270  itg2cnlem1  25271  ibl0  25296  iblcnlem1  25297  i1fibl  25317  itgeqa  25323  itgcn  25354  dvcmul  25453  dvcmulf  25454  dvexp3  25487  dvef  25489  rolle  25499  dveq0  25509  dv11cn  25510  tdeglem4  25569  tdeglem4OLD  25570  elply2  25702  elplyd  25708  ply1term  25710  ply0  25714  plyeq0  25717  plypf1  25718  plymullem  25722  dgrlt  25772  plymul0or  25786  dvply1  25789  plydivlem4  25801  elqaalem2  25825  iaa  25830  aareccl  25831  aannenlem2  25834  tayl0  25866  taylpfval  25869  dvtaylp  25874  pserdvlem2  25932  abelthlem9  25944  logtayl  26160  cxplogb  26281  leibpilem2  26436  leibpi  26437  jensenlem2  26482  jensen  26483  amgmlem  26484  amgm  26485  igamval  26541  vmaval  26607  vmaf  26613  muval  26626  dchrelbas2  26730  dchrinvcl  26746  dchrptlem2  26758  lgseisenlem4  26871  addsqnreup  26936  pntrlog2bndlem4  27073  pntrlog2bndlem5  27074  padicval  27110  padicabv  27123  ostth1  27126  axlowdimlem8  28197  axlowdimlem9  28198  axlowdimlem10  28199  axlowdimlem11  28200  axlowdimlem12  28201  axlowdimlem13  28202  axlowdimlem17  28206  uspgr1ewop  28495  usgr2v1e2w  28499  umgr2v2eedg  28771  umgr2v2e  28772  umgr2v2evd2  28774  wlkl1loop  28885  2wlklem  28914  usgr2trlncl  29007  2wlkdlem4  29172  2wlkdlem5  29173  2pthdlem1  29174  2wlkdlem10  29179  umgrwwlks2on  29201  rusgrnumwwlkl1  29212  clwwlkn2  29287  0spth  29369  1wlkdlem4  29383  wlk2v2elem1  29398  3wlkdlem4  29405  3wlkdlem5  29406  3pthdlem1  29407  3wlkdlem10  29412  upgr3v3e3cycl  29423  upgr4cycl4dv4e  29428  eulerpathpr  29483  konigsberglem4  29498  konigsberglem5  29499  wlkl0  29610  occllem  30544  0cnfn  31221  0lnfn  31226  nmfn0  31228  nmcexi  31267  nlelchi  31302  fprodex01  32019  s2rn  32098  s3rn  32100  xrge0tsmsd  32197  cyc2fv1  32268  cyc3fv1  32284  cyc3evpm  32297  sgnsval  32308  sgnsf  32309  xrge0iif1  32907  xrge0mulc1cn  32910  gsumesum  33046  esumpfinval  33062  esumpfinvalf  33063  ddeval1  33221  ddeval0  33222  ddemeas  33223  eulerpartlemt  33359  coinfliprv  33470  sgncl  33526  plymul02  33546  plymulx  33548  signsw0glem  33553  signsw0g  33556  signswmnd  33557  signswrid  33558  prodfzo03  33604  circlevma  33643  circlemethhgt  33644  hgt750lemg  33655  hgt750lemb  33657  hgt750lema  33658  hgt750leme  33659  tgoldbachgtde  33661  tgoldbachgt  33664  cvmliftlem4  34268  cvmliftlem5  34269  poimirlem1  36478  poimirlem2  36479  poimirlem3  36480  poimirlem4  36481  poimirlem5  36482  poimirlem6  36483  poimirlem7  36484  poimirlem11  36488  poimirlem12  36489  poimirlem16  36493  poimirlem17  36494  poimirlem19  36496  poimirlem20  36497  poimirlem22  36499  poimirlem23  36500  poimirlem24  36501  poimirlem25  36502  poimirlem28  36505  poimirlem29  36506  poimirlem31  36508  poimirlem32  36509  poimir  36510  broucube  36511  mblfinlem2  36515  mblfinlem3  36516  ismblfin  36518  itg2addnclem  36528  itg2addnclem3  36530  itg2addnc  36531  ftc1anclem3  36552  ftc1anclem5  36554  ftc1anclem7  36556  ftc1anclem8  36557  ftc1anc  36558  dvacos  36562  prdsbnd  36650  heiborlem10  36677  renegclALT  37822  aks4d1p1p4  40925  0prjspnlem  41362  0prjspnrel  41366  diophrw  41483  monotoddzzfi  41667  zindbi  41671  mncn0  41867  aaitgo  41890  flcidc  41902  dfrcl4  42413  fvrcllb0d  42430  fvrcllb0da  42431  iunrelexp0  42439  corclrcl  42444  relexp0idm  42452  dfrtrcl4  42475  corcltrcl  42476  cotrclrcl  42479  ofsubid  43069  lhe4.4ex1a  43074  dvsconst  43075  dvconstbi  43079  binomcxplemnn0  43094  binomcxplemdvbinom  43098  binomcxplemnotnn0  43101  n0p  43716  climrec  44306  limsup10exlem  44475  dvnmptdivc  44641  dvnmul  44646  stoweidlem55  44758  fourierdlem62  44871  fourierdlem104  44913  fouriersw  44934  ovnval2  45248  hoidmvval  45280  tworepnotupword  45587  fun2dmnopgexmpl  45979  el1fzopredsuc  46020  nn0mnd  46576  zlmodzxzel  46985  zlmodzxz0  46986  zlmodzxzscm  46987  zlmodzxzadd  46988  zlmodzxznm  47132  zlmodzxzldeplem  47133  zlmodzxzldeplem2  47136  blen0  47212  nn0sumshdiglemB  47260  fv1arycl  47277  1arympt1  47278  1arympt1fv  47279  1arymaptf1  47282  1arymaptfo  47283  fv2arycl  47288  2arympt  47289  2arymptfv  47290  2arymaptf1  47293  2arymaptfo  47294  ehl2eudisval0  47365  2sphere0  47390  line2ylem  47391  line2  47392  line2x  47394  line2y  47395  ex-gt  47727  ex-gte  47728  aacllem  47802