Theorem c0ex 11284

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

Syntax hints:   ∈ wcel 2108  Vcvv 3488  ℂcc 11182  0cc0 11184

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-mulcl 11246  ax-i2m1 11252

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490

This theorem is referenced by:  ofsubeq0  12290  ofsubge0  12292  elnn0  12555  un0mulcl  12587  fcdmnn0supp  12609  fcdmnn0fsupp  12610  fcdmnn0suppg  12611  fcdmnn0fsuppg  12612  nn0ssz  12662  nn0ind-raph  12743  xaddval  13285  xmulval  13287  ser0f  14106  facnn  14324  fac0  14325  bcval  14353  prhash2ex  14448  wrdexb  14573  s1rn  14647  eqs1  14660  repsw1  14831  cshw1  14870  s1co  14882  funcnvs2  14962  funcnvs3  14963  funcnvs4  14964  wrdlen2i  14991  wrd2pr2op  14992  wrd3tpop  14997  wwlktovf1  15006  wrdl3s3  15011  sgnval  15137  iserge0  15709  sum0  15769  sumz  15770  fsumss  15773  fsumser  15778  isumless  15893  geomulcvg  15924  rpnnen2lem1  16262  ruclem4  16282  ruclem8  16285  ruclem11  16288  0bits  16485  gcdval  16542  lcmval  16639  lcmfpr  16674  lcmfunsnlem2  16687  prmreclem2  16964  prmreclem5  16967  vdwapun  17021  smndex1n0mnd  18947  mgmnsgrpex  18966  odval  19576  odf  19579  gexval  19620  telgsumfz0  20034  telgsum  20036  srgbinom  20258  abvtrivd  20855  pzriprnglem4  21518  pzriprnglem5  21519  pzriprnglem7  21521  pzriprnglem9  21523  pzriprnglem10  21524  snifpsrbag  21963  psrbaglesupp  21965  psrbaglefi  21969  mplcoe5  22081  mplbas2  22083  ltbwe  22085  psrbag0  22109  psrbagev1  22124  mhpmulcl  22176  psdmplcl  22189  cply1coe0bi  22327  m2cpminvid2lem  22781  pmatcollpw3fi1lem1  22813  pmatcollpw3fi1lem2  22814  pmatcollpw3fi1  22815  idpm2idmp  22828  prdsdsf  24398  prdsxmetlem  24399  prdsmet  24401  imasdsf1olem  24404  prdsbl  24525  xrge0gsumle  24874  xrge0tsms  24875  xrhmeo  24996  pcopt  25074  pcopt2  25075  pcoass  25076  rrxcph  25445  rrx0el  25451  rrxbasefi  25463  ovoliunnul  25561  ovolicc1  25570  vitalilem5  25666  mbfpos  25705  0pval  25725  0pledm  25727  i1f1lem  25743  i1f1  25744  itg11  25745  itg1addlem3  25752  itg1addlem4  25753  itg1addlem4OLD  25754  i1fres  25760  itg1climres  25769  mbfi1fseqlem4  25773  mbfi1fseqlem6  25775  mbfi1flimlem  25777  mbfi1flim  25778  xrge0f  25786  itg2ge0  25790  itg2uba  25798  itg2splitlem  25803  itg2monolem1  25805  itg2gt0  25815  itg2cnlem1  25816  ibl0  25842  iblcnlem1  25843  i1fibl  25863  itgeqa  25869  itgcn  25900  dvcmul  26001  dvcmulf  26002  dvexp3  26036  dvef  26038  rolle  26048  dveq0  26059  dv11cn  26060  tdeglem4  26119  elply2  26255  elplyd  26261  ply1term  26263  ply0  26267  plyeq0  26270  plypf1  26271  plymullem  26275  dgrlt  26326  plymul0or  26340  dvply1  26343  plydivlem4  26356  elqaalem2  26380  iaa  26385  aareccl  26386  aannenlem2  26389  tayl0  26421  taylpfval  26424  dvtaylp  26430  pserdvlem2  26490  abelthlem9  26502  logtayl  26720  cxplogb  26847  leibpilem2  27002  leibpi  27003  jensenlem2  27049  jensen  27050  amgmlem  27051  amgm  27052  igamval  27108  vmaval  27174  vmaf  27180  muval  27193  dchrelbas2  27299  dchrinvcl  27315  dchrptlem2  27327  lgseisenlem4  27440  addsqnreup  27505  pntrlog2bndlem4  27642  pntrlog2bndlem5  27643  padicval  27679  padicabv  27692  ostth1  27695  axlowdimlem8  28982  axlowdimlem9  28983  axlowdimlem10  28984  axlowdimlem11  28985  axlowdimlem12  28986  axlowdimlem13  28987  axlowdimlem17  28991  uspgr1ewop  29283  usgr2v1e2w  29287  umgr2v2eedg  29560  umgr2v2e  29561  umgr2v2evd2  29563  wlkl1loop  29674  2wlklem  29703  usgr2trlncl  29796  2wlkdlem4  29961  2wlkdlem5  29962  2pthdlem1  29963  2wlkdlem10  29968  umgrwwlks2on  29990  rusgrnumwwlkl1  30001  clwwlkn2  30076  0spth  30158  1wlkdlem4  30172  wlk2v2elem1  30187  3wlkdlem4  30194  3wlkdlem5  30195  3pthdlem1  30196  3wlkdlem10  30201  upgr3v3e3cycl  30212  upgr4cycl4dv4e  30217  eulerpathpr  30272  konigsberglem4  30287  konigsberglem5  30288  wlkl0  30399  occllem  31335  0cnfn  32012  0lnfn  32017  nmfn0  32019  nmcexi  32058  nlelchi  32093  fprodex01  32829  s2rnOLD  32910  s3rnOLD  32912  xrge0tsmsd  33041  cyc2fv1  33114  cyc3fv1  33130  cyc3evpm  33143  sgnsval  33154  sgnsf  33155  constr01  33732  constrss  33733  constrconj  33735  xrge0iif1  33884  xrge0mulc1cn  33887  gsumesum  34023  esumpfinval  34039  esumpfinvalf  34040  ddeval1  34198  ddeval0  34199  ddemeas  34200  eulerpartlemt  34336  coinfliprv  34447  sgncl  34503  plymul02  34523  plymulx  34525  signsw0glem  34530  signsw0g  34533  signswmnd  34534  signswrid  34535  prodfzo03  34580  circlevma  34619  circlemethhgt  34620  hgt750lemg  34631  hgt750lemb  34633  hgt750lema  34634  hgt750leme  34635  tgoldbachgtde  34637  tgoldbachgt  34640  cvmliftlem4  35256  cvmliftlem5  35257  poimirlem1  37581  poimirlem2  37582  poimirlem3  37583  poimirlem4  37584  poimirlem5  37585  poimirlem6  37586  poimirlem7  37587  poimirlem11  37591  poimirlem12  37592  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem22  37602  poimirlem23  37603  poimirlem24  37604  poimirlem25  37605  poimirlem28  37608  poimirlem29  37609  poimirlem31  37611  poimirlem32  37612  poimir  37613  broucube  37614  mblfinlem2  37618  mblfinlem3  37619  ismblfin  37621  itg2addnclem  37631  itg2addnclem3  37633  itg2addnc  37634  ftc1anclem3  37655  ftc1anclem5  37657  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  dvacos  37665  prdsbnd  37753  heiborlem10  37780  renegclALT  38919  aks4d1p1p4  42028  aks6d1c7lem1  42137  0prjspnlem  42578  0prjspnrel  42582  diophrw  42715  monotoddzzfi  42899  zindbi  42903  mncn0  43096  aaitgo  43119  flcidc  43131  dfrcl4  43638  fvrcllb0d  43655  fvrcllb0da  43656  iunrelexp0  43664  corclrcl  43669  relexp0idm  43677  dfrtrcl4  43700  corcltrcl  43701  cotrclrcl  43704  ofsubid  44293  lhe4.4ex1a  44298  dvsconst  44299  dvconstbi  44303  binomcxplemnn0  44318  binomcxplemdvbinom  44322  binomcxplemnotnn0  44325  n0p  44945  climrec  45524  limsup10exlem  45693  dvnmptdivc  45859  dvnmul  45864  stoweidlem55  45976  fourierdlem62  46089  fourierdlem104  46131  fouriersw  46152  ovnval2  46466  hoidmvval  46498  tworepnotupword  46805  fun2dmnopgexmpl  47199  el1fzopredsuc  47240  usgrexmpl1lem  47836  usgrexmpl1tri  47840  usgrexmpl2lem  47841  usgrexmpl2nb0  47846  usgrexmpl2nb1  47847  usgrexmpl2nb2  47848  usgrexmpl2nb3  47849  usgrexmpl2nb4  47850  usgrexmpl2nb5  47851  usgrexmpl2trifr  47852  nn0mnd  47902  zlmodzxzel  48080  zlmodzxz0  48081  zlmodzxzscm  48082  zlmodzxzadd  48083  zlmodzxznm  48226  zlmodzxzldeplem  48227  zlmodzxzldeplem2  48230  blen0  48306  nn0sumshdiglemB  48354  fv1arycl  48371  1arympt1  48372  1arympt1fv  48373  1arymaptf1  48376  1arymaptfo  48377  fv2arycl  48382  2arympt  48383  2arymptfv  48384  2arymaptf1  48387  2arymaptfo  48388  ehl2eudisval0  48459  2sphere0  48484  line2ylem  48485  line2  48486  line2x  48488  line2y  48489  ex-gt  48820  ex-gte  48821  aacllem  48895