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  37822  poimirlem2  37823  poimirlem3  37824  poimirlem4  37825  poimirlem5  37826  poimirlem6  37827  poimirlem7  37828  poimirlem11  37832  poimirlem12  37833  poimirlem16  37837  poimirlem17  37838  poimirlem19  37840  poimirlem20  37841  poimirlem22  37843  poimirlem23  37844  poimirlem24  37845  poimirlem25  37846  poimirlem28  37849  poimirlem29  37850  poimirlem31  37852  poimirlem32  37853  poimir  37854  broucube  37855  mblfinlem2  37859  mblfinlem3  37860  ismblfin  37862  itg2addnclem  37872  itg2addnclem3  37874  itg2addnc  37875  ftc1anclem3  37896  ftc1anclem5  37898  ftc1anclem7  37900  ftc1anclem8  37901  ftc1anc  37902  dvacos  37906  prdsbnd  37994  heiborlem10  38021  renegclALT  39223  aks4d1p1p4  42325  aks6d1c7lem1  42434  0prjspnlem  42866  0prjspnrel  42870  diophrw  43001  monotoddzzfi  43184  zindbi  43188  mncn0  43381  aaitgo  43404  flcidc  43412  dfrcl4  43917  fvrcllb0d  43934  fvrcllb0da  43935  iunrelexp0  43943  corclrcl  43948  relexp0idm  43956  dfrtrcl4  43979  corcltrcl  43980  cotrclrcl  43983  ofsubid  44565  lhe4.4ex1a  44570  dvsconst  44571  dvconstbi  44575  binomcxplemnn0  44590  binomcxplemdvbinom  44594  binomcxplemnotnn0  44597  n0p  45290  climrec  45849  limsup10exlem  46016  dvnmptdivc  46182  dvnmul  46187  stoweidlem55  46299  fourierdlem62  46412  fourierdlem104  46454  fouriersw  46475  ovnval2  46789  hoidmvval  46821  lambert0  47133  tannpoly  47136  sinnpoly  47137  fun2dmnopgexmpl  47530  el1fzopredsuc  47571  cycl3grtrilem  48192  stgrusgra  48205  stgr1  48207  stgrnbgr0  48210  isubgr3stgrlem3  48214  isubgr3stgrlem7  48218  usgrexmpl1lem  48267  usgrexmpl1tri  48271  usgrexmpl2lem  48272  usgrexmpl2nb0  48277  usgrexmpl2nb1  48278  usgrexmpl2nb2  48279  usgrexmpl2nb3  48280  usgrexmpl2nb4  48281  usgrexmpl2nb5  48282  usgrexmpl2trifr  48283  gpgiedgdmellem  48292  gpgvtx0  48299  opgpgvtx  48301  gpgedgvtx0  48307  gpgvtxedg0  48309  gpgvtxedg1  48310  gpgedgiov  48311  gpgedg2ov  48312  gpg5nbgrvtx03starlem1  48314  gpg5nbgrvtx03starlem2  48315  gpg5nbgrvtx03starlem3  48316  gpg5nbgrvtx13starlem1  48317  gpg5nbgrvtx13starlem3  48319  gpg3nbgrvtx0  48322  gpg3nbgrvtx0ALT  48323  gpg3nbgrvtx1  48324  gpgcubic  48325  gpg5nbgr3star  48327  gpg3kgrtriex  48335  gpgprismgr4cycllem2  48342  gpgprismgr4cycllem3  48343  gpgprismgr4cycllem7  48347  gpgprismgr4cycllem9  48349  pgnioedg1  48354  pgnioedg2  48355  pgnioedg3  48356  pgnioedg4  48357  pgnioedg5  48358  pgnbgreunbgrlem1  48359  pgnbgreunbgrlem2lem1  48360  pgnbgreunbgrlem2lem2  48361  pgnbgreunbgrlem2lem3  48362  pgnbgreunbgrlem3  48364  pgnbgreunbgrlem5lem3  48368  pgnbgreunbgrlem5  48369  pgnbgreunbgrlem6  48370  gpg5edgnedg  48376  nn0mnd  48425  zlmodzxzel  48601  zlmodzxz0  48602  zlmodzxzscm  48603  zlmodzxzadd  48604  zlmodzxznm  48743  zlmodzxzldeplem  48744  zlmodzxzldeplem2  48747  blen0  48818  nn0sumshdiglemB  48866  fv1arycl  48883  1arympt1  48884  1arympt1fv  48885  1arymaptf1  48888  1arymaptfo  48889  fv2arycl  48894  2arympt  48895  2arymptfv  48896  2arymaptf1  48899  2arymaptfo  48900  ehl2eudisval0  48971  2sphere0  48996  line2ylem  48997  line2  48998  line2x  49000  line2y  49001  ex-gt  49973  ex-gte  49974  aacllem  50046