Theorem c0ex 11126

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

Syntax hints:   ∈ wcel 2113  Vcvv 3440  ℂcc 11024  0cc0 11026

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-mulcl 11088  ax-i2m1 11094

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442

This theorem is referenced by:  ofsubeq0  12142  ofsubge0  12144  elnn0  12403  un0mulcl  12435  fcdmnn0supp  12458  fcdmnn0fsupp  12459  fcdmnn0suppg  12460  fcdmnn0fsuppg  12461  nn0ssz  12511  nn0ind-raph  12592  xaddval  13138  xmulval  13140  ser0f  13978  facnn  14198  fac0  14199  bcval  14227  prhash2ex  14322  wrdexb  14448  s1rn  14523  eqs1  14536  repsw1  14706  cshw1  14745  s1co  14756  funcnvs2  14836  funcnvs3  14837  funcnvs4  14838  wrdlen2i  14865  wrd2pr2op  14866  wrd3tpop  14871  wwlktovf1  14880  wrdl3s3  14885  sgnval  15011  iserge0  15584  sum0  15644  sumz  15645  fsumss  15648  fsumser  15653  isumless  15768  geomulcvg  15799  rpnnen2lem1  16139  ruclem4  16159  ruclem8  16162  ruclem11  16165  0bits  16366  gcdval  16423  lcmval  16519  lcmfpr  16554  lcmfunsnlem2  16567  prmreclem2  16845  prmreclem5  16848  vdwapun  16902  smndex1n0mnd  18837  mgmnsgrpex  18856  odval  19463  odf  19466  gexval  19507  telgsumfz0  19921  telgsum  19923  srgbinom  20166  abvtrivd  20765  pzriprnglem4  21439  pzriprnglem5  21440  pzriprnglem7  21442  pzriprnglem9  21444  pzriprnglem10  21445  snifpsrbag  21876  psrbaglesupp  21878  psrbaglefi  21882  mplcoe5  21995  mplbas2  21997  ltbwe  21999  psrbag0  22017  psrbagev1  22032  mhpmulcl  22092  psdmplcl  22105  psdmvr  22112  cply1coe0bi  22246  m2cpminvid2lem  22698  pmatcollpw3fi1lem1  22730  pmatcollpw3fi1lem2  22731  pmatcollpw3fi1  22732  idpm2idmp  22745  prdsdsf  24311  prdsxmetlem  24312  prdsmet  24314  imasdsf1olem  24317  prdsbl  24435  xrge0gsumle  24778  xrge0tsms  24779  xrhmeo  24900  pcopt  24978  pcopt2  24979  pcoass  24980  rrxcph  25348  rrx0el  25354  rrxbasefi  25366  ovoliunnul  25464  ovolicc1  25473  vitalilem5  25569  mbfpos  25608  0pval  25628  0pledm  25630  i1f1lem  25646  i1f1  25647  itg11  25648  itg1addlem3  25655  itg1addlem4  25656  i1fres  25662  itg1climres  25671  mbfi1fseqlem4  25675  mbfi1fseqlem6  25677  mbfi1flimlem  25679  mbfi1flim  25680  xrge0f  25688  itg2ge0  25692  itg2uba  25700  itg2splitlem  25705  itg2monolem1  25707  itg2gt0  25717  itg2cnlem1  25718  ibl0  25744  iblcnlem1  25745  i1fibl  25765  itgeqa  25771  itgcn  25802  dvcmul  25903  dvcmulf  25904  dvexp3  25938  dvef  25940  rolle  25950  dveq0  25961  dv11cn  25962  tdeglem4  26021  elply2  26157  elplyd  26163  ply1term  26165  ply0  26169  plyeq0  26172  plypf1  26173  plymullem  26177  dgrlt  26228  plymul0or  26244  dvply1  26247  plydivlem4  26260  elqaalem2  26284  iaa  26289  aareccl  26290  aannenlem2  26293  tayl0  26325  taylpfval  26328  dvtaylp  26334  pserdvlem2  26394  abelthlem9  26406  logtayl  26625  cxplogb  26752  leibpilem2  26907  leibpi  26908  jensenlem2  26954  jensen  26955  amgmlem  26956  amgm  26957  igamval  27013  vmaval  27079  vmaf  27085  muval  27098  dchrelbas2  27204  dchrinvcl  27220  dchrptlem2  27232  lgseisenlem4  27345  addsqnreup  27410  pntrlog2bndlem4  27547  pntrlog2bndlem5  27548  padicval  27584  padicabv  27597  ostth1  27600  axlowdimlem8  29022  axlowdimlem9  29023  axlowdimlem10  29024  axlowdimlem11  29025  axlowdimlem12  29026  axlowdimlem13  29027  axlowdimlem17  29031  uspgr1ewop  29321  usgr2v1e2w  29325  umgr2v2eedg  29598  umgr2v2e  29599  umgr2v2evd2  29601  wlkl1loop  29711  2wlklem  29739  usgr2trlncl  29833  2wlkdlem4  30001  2wlkdlem5  30002  2pthdlem1  30003  2wlkdlem10  30008  usgrwwlks2on  30031  umgrwwlks2on  30032  rusgrnumwwlkl1  30044  clwwlkn2  30119  0spth  30201  1wlkdlem4  30215  wlk2v2elem1  30230  3wlkdlem4  30237  3wlkdlem5  30238  3pthdlem1  30239  3wlkdlem10  30244  upgr3v3e3cycl  30255  upgr4cycl4dv4e  30260  eulerpathpr  30315  konigsberglem4  30330  konigsberglem5  30331  wlkl0  30442  occllem  31378  0cnfn  32055  0lnfn  32060  nmfn0  32062  nmcexi  32101  nlelchi  32136  fprodex01  32906  sgncl  32912  indsupp  32949  indfsd  32950  indfsid  32951  s2rnOLD  33026  s3rnOLD  33028  gsummulsubdishift1  33151  gsummulsubdishift2s  33154  xrge0tsmsd  33155  cyc2fv1  33203  cyc3fv1  33219  cyc3evpm  33232  sgnsval  33243  sgnsf  33244  elrgspnlem1  33324  elrgspnlem4  33327  gsumind  33426  extvfvvcl  33700  extvfvcl  33701  esplyfval0  33722  esplysply  33729  esplyind  33731  vieta  33736  constr01  33899  constrss  33900  constrconj  33902  constrextdg2lem  33905  nn0constr  33918  xrge0iif1  34095  xrge0mulc1cn  34098  gsumesum  34216  esumpfinval  34232  esumpfinvalf  34233  ddeval1  34391  ddeval0  34392  ddemeas  34393  eulerpartlemt  34528  coinfliprv  34640  plymul02  34703  plymulx  34705  signsw0glem  34710  signsw0g  34713  signswmnd  34714  signswrid  34715  prodfzo03  34760  circlevma  34799  circlemethhgt  34800  hgt750lemg  34811  hgt750lemb  34813  hgt750lema  34814  hgt750leme  34815  tgoldbachgtde  34817  tgoldbachgt  34820  cvmliftlem4  35482  cvmliftlem5  35483  poimirlem1  37818  poimirlem2  37819  poimirlem3  37820  poimirlem4  37821  poimirlem5  37822  poimirlem6  37823  poimirlem7  37824  poimirlem11  37828  poimirlem12  37829  poimirlem16  37833  poimirlem17  37834  poimirlem19  37836  poimirlem20  37837  poimirlem22  37839  poimirlem23  37840  poimirlem24  37841  poimirlem25  37842  poimirlem28  37845  poimirlem29  37846  poimirlem31  37848  poimirlem32  37849  poimir  37850  broucube  37851  mblfinlem2  37855  mblfinlem3  37856  ismblfin  37858  itg2addnclem  37868  itg2addnclem3  37870  itg2addnc  37871  ftc1anclem3  37892  ftc1anclem5  37894  ftc1anclem7  37896  ftc1anclem8  37897  ftc1anc  37898  dvacos  37902  prdsbnd  37990  heiborlem10  38017  renegclALT  39219  aks4d1p1p4  42321  aks6d1c7lem1  42430  0prjspnlem  42862  0prjspnrel  42866  diophrw  42997  monotoddzzfi  43180  zindbi  43184  mncn0  43377  aaitgo  43400  flcidc  43408  dfrcl4  43913  fvrcllb0d  43930  fvrcllb0da  43931  iunrelexp0  43939  corclrcl  43944  relexp0idm  43952  dfrtrcl4  43975  corcltrcl  43976  cotrclrcl  43979  ofsubid  44561  lhe4.4ex1a  44566  dvsconst  44567  dvconstbi  44571  binomcxplemnn0  44586  binomcxplemdvbinom  44590  binomcxplemnotnn0  44593  n0p  45286  climrec  45845  limsup10exlem  46012  dvnmptdivc  46178  dvnmul  46183  stoweidlem55  46295  fourierdlem62  46408  fourierdlem104  46450  fouriersw  46471  ovnval2  46785  hoidmvval  46817  lambert0  47129  tannpoly  47132  sinnpoly  47133  fun2dmnopgexmpl  47526  el1fzopredsuc  47567  cycl3grtrilem  48188  stgrusgra  48201  stgr1  48203  stgrnbgr0  48206  isubgr3stgrlem3  48210  isubgr3stgrlem7  48214  usgrexmpl1lem  48263  usgrexmpl1tri  48267  usgrexmpl2lem  48268  usgrexmpl2nb0  48273  usgrexmpl2nb1  48274  usgrexmpl2nb2  48275  usgrexmpl2nb3  48276  usgrexmpl2nb4  48277  usgrexmpl2nb5  48278  usgrexmpl2trifr  48279  gpgiedgdmellem  48288  gpgvtx0  48295  opgpgvtx  48297  gpgedgvtx0  48303  gpgvtxedg0  48305  gpgvtxedg1  48306  gpgedgiov  48307  gpgedg2ov  48308  gpg5nbgrvtx03starlem1  48310  gpg5nbgrvtx03starlem2  48311  gpg5nbgrvtx03starlem3  48312  gpg5nbgrvtx13starlem1  48313  gpg5nbgrvtx13starlem3  48315  gpg3nbgrvtx0  48318  gpg3nbgrvtx0ALT  48319  gpg3nbgrvtx1  48320  gpgcubic  48321  gpg5nbgr3star  48323  gpg3kgrtriex  48331  gpgprismgr4cycllem2  48338  gpgprismgr4cycllem3  48339  gpgprismgr4cycllem7  48343  gpgprismgr4cycllem9  48345  pgnioedg1  48350  pgnioedg2  48351  pgnioedg3  48352  pgnioedg4  48353  pgnioedg5  48354  pgnbgreunbgrlem1  48355  pgnbgreunbgrlem2lem1  48356  pgnbgreunbgrlem2lem2  48357  pgnbgreunbgrlem2lem3  48358  pgnbgreunbgrlem3  48360  pgnbgreunbgrlem5lem3  48364  pgnbgreunbgrlem5  48365  pgnbgreunbgrlem6  48366  gpg5edgnedg  48372  nn0mnd  48421  zlmodzxzel  48597  zlmodzxz0  48598  zlmodzxzscm  48599  zlmodzxzadd  48600  zlmodzxznm  48739  zlmodzxzldeplem  48740  zlmodzxzldeplem2  48743  blen0  48814  nn0sumshdiglemB  48862  fv1arycl  48879  1arympt1  48880  1arympt1fv  48881  1arymaptf1  48884  1arymaptfo  48885  fv2arycl  48890  2arympt  48891  2arymptfv  48892  2arymaptf1  48895  2arymaptfo  48896  ehl2eudisval0  48967  2sphere0  48992  line2ylem  48993  line2  48994  line2x  48996  line2y  48997  ex-gt  49969  ex-gte  49970  aacllem  50042