Theorem c0ex 11129

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

Syntax hints:   ∈ wcel 2114  Vcvv 3430  ℂcc 11027  0cc0 11029

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-mulcl 11091  ax-i2m1 11097

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432

This theorem is referenced by:  ofsubeq0  12147  ofsubge0  12149  elnn0  12430  un0mulcl  12462  fcdmnn0supp  12485  fcdmnn0fsupp  12486  fcdmnn0suppg  12487  fcdmnn0fsuppg  12488  nn0ssz  12538  nn0ind-raph  12620  xaddval  13166  xmulval  13168  ser0f  14008  facnn  14228  fac0  14229  bcval  14257  prhash2ex  14352  wrdexb  14478  s1rn  14553  eqs1  14566  repsw1  14736  cshw1  14775  s1co  14786  funcnvs2  14866  funcnvs3  14867  funcnvs4  14868  wrdlen2i  14895  wrd2pr2op  14896  wrd3tpop  14901  wwlktovf1  14910  wrdl3s3  14915  sgnval  15041  iserge0  15614  sum0  15674  sumz  15675  fsumss  15678  fsumser  15683  isumless  15801  geomulcvg  15832  rpnnen2lem1  16172  ruclem4  16192  ruclem8  16195  ruclem11  16198  0bits  16399  gcdval  16456  lcmval  16552  lcmfpr  16587  lcmfunsnlem2  16600  prmreclem2  16879  prmreclem5  16882  vdwapun  16936  smndex1n0mnd  18874  mgmnsgrpex  18893  odval  19500  odf  19503  gexval  19544  telgsumfz0  19958  telgsum  19960  srgbinom  20203  abvtrivd  20800  pzriprnglem4  21474  pzriprnglem5  21475  pzriprnglem7  21477  pzriprnglem9  21479  pzriprnglem10  21480  snifpsrbag  21910  psrbaglesupp  21912  psrbaglefi  21916  mplcoe5  22028  mplbas2  22030  ltbwe  22032  psrbag0  22050  psrbagev1  22065  mhpmulcl  22125  psdmplcl  22138  psdmvr  22145  cply1coe0bi  22277  m2cpminvid2lem  22729  pmatcollpw3fi1lem1  22761  pmatcollpw3fi1lem2  22762  pmatcollpw3fi1  22763  idpm2idmp  22776  prdsdsf  24342  prdsxmetlem  24343  prdsmet  24345  imasdsf1olem  24348  prdsbl  24466  xrge0gsumle  24809  xrge0tsms  24810  xrhmeo  24923  pcopt  24999  pcopt2  25000  pcoass  25001  rrxcph  25369  rrx0el  25375  rrxbasefi  25387  ovoliunnul  25484  ovolicc1  25493  vitalilem5  25589  mbfpos  25628  0pval  25648  0pledm  25650  i1f1lem  25666  i1f1  25667  itg11  25668  itg1addlem3  25675  itg1addlem4  25676  i1fres  25682  itg1climres  25691  mbfi1fseqlem4  25695  mbfi1fseqlem6  25697  mbfi1flimlem  25699  mbfi1flim  25700  xrge0f  25708  itg2ge0  25712  itg2uba  25720  itg2splitlem  25725  itg2monolem1  25727  itg2gt0  25737  itg2cnlem1  25738  ibl0  25764  iblcnlem1  25765  i1fibl  25785  itgeqa  25791  itgcn  25822  dvcmul  25921  dvcmulf  25922  dvexp3  25955  dvef  25957  rolle  25967  dveq0  25977  dv11cn  25978  tdeglem4  26035  elply2  26171  elplyd  26177  ply1term  26179  ply0  26183  plyeq0  26186  plypf1  26187  plymullem  26191  dgrlt  26241  plymul0or  26257  dvply1  26260  plydivlem4  26273  elqaalem2  26297  iaa  26302  aareccl  26303  aannenlem2  26306  tayl0  26338  taylpfval  26341  dvtaylp  26347  pserdvlem2  26406  abelthlem9  26418  logtayl  26637  cxplogb  26763  leibpilem2  26918  leibpi  26919  jensenlem2  26965  jensen  26966  amgmlem  26967  amgm  26968  igamval  27024  vmaval  27090  vmaf  27096  muval  27109  dchrelbas2  27214  dchrinvcl  27230  dchrptlem2  27242  lgseisenlem4  27355  addsqnreup  27420  pntrlog2bndlem4  27557  pntrlog2bndlem5  27558  padicval  27594  padicabv  27607  ostth1  27610  axlowdimlem8  29032  axlowdimlem9  29033  axlowdimlem10  29034  axlowdimlem11  29035  axlowdimlem12  29036  axlowdimlem13  29037  axlowdimlem17  29041  uspgr1ewop  29331  usgr2v1e2w  29335  umgr2v2eedg  29608  umgr2v2e  29609  umgr2v2evd2  29611  wlkl1loop  29721  2wlklem  29749  usgr2trlncl  29843  2wlkdlem4  30011  2wlkdlem5  30012  2pthdlem1  30013  2wlkdlem10  30018  usgrwwlks2on  30041  umgrwwlks2on  30042  rusgrnumwwlkl1  30054  clwwlkn2  30129  0spth  30211  1wlkdlem4  30225  wlk2v2elem1  30240  3wlkdlem4  30247  3wlkdlem5  30248  3pthdlem1  30249  3wlkdlem10  30254  upgr3v3e3cycl  30265  upgr4cycl4dv4e  30270  eulerpathpr  30325  konigsberglem4  30340  konigsberglem5  30341  wlkl0  30452  occllem  31389  0cnfn  32066  0lnfn  32071  nmfn0  32073  nmcexi  32112  nlelchi  32147  fprodex01  32913  sgncl  32919  indsupp  32942  indfsd  32943  indfsid  32944  s2rnOLD  33019  s3rnOLD  33021  gsummulsubdishift1  33144  gsummulsubdishift2s  33147  xrge0tsmsd  33149  cyc2fv1  33197  cyc3fv1  33213  cyc3evpm  33226  sgnsval  33237  sgnsf  33238  elrgspnlem1  33318  elrgspnlem4  33321  gsumind  33420  extvfvvcl  33694  extvfvcl  33695  esplyfval0  33723  esplysply  33730  esplyind  33734  vieta  33739  constr01  33902  constrss  33903  constrconj  33905  constrextdg2lem  33908  nn0constr  33921  xrge0iif1  34098  xrge0mulc1cn  34101  gsumesum  34219  esumpfinval  34235  esumpfinvalf  34236  ddeval1  34394  ddeval0  34395  ddemeas  34396  eulerpartlemt  34531  coinfliprv  34643  plymul02  34706  plymulx  34708  signsw0glem  34713  signsw0g  34716  signswmnd  34717  signswrid  34718  prodfzo03  34763  circlevma  34802  circlemethhgt  34803  hgt750lemg  34814  hgt750lemb  34816  hgt750lema  34817  hgt750leme  34818  tgoldbachgtde  34820  tgoldbachgt  34823  cvmliftlem4  35486  cvmliftlem5  35487  poimirlem1  37956  poimirlem2  37957  poimirlem3  37958  poimirlem4  37959  poimirlem5  37960  poimirlem6  37961  poimirlem7  37962  poimirlem11  37966  poimirlem12  37967  poimirlem16  37971  poimirlem17  37972  poimirlem19  37974  poimirlem20  37975  poimirlem22  37977  poimirlem23  37978  poimirlem24  37979  poimirlem25  37980  poimirlem28  37983  poimirlem29  37984  poimirlem31  37986  poimirlem32  37987  poimir  37988  broucube  37989  mblfinlem2  37993  mblfinlem3  37994  ismblfin  37996  itg2addnclem  38006  itg2addnclem3  38008  itg2addnc  38009  ftc1anclem3  38030  ftc1anclem5  38032  ftc1anclem7  38034  ftc1anclem8  38035  ftc1anc  38036  dvacos  38040  prdsbnd  38128  heiborlem10  38155  renegclALT  39423  aks4d1p1p4  42524  aks6d1c7lem1  42633  0prjspnlem  43070  0prjspnrel  43074  diophrw  43205  monotoddzzfi  43388  zindbi  43392  mncn0  43585  aaitgo  43608  flcidc  43616  dfrcl4  44121  fvrcllb0d  44138  fvrcllb0da  44139  iunrelexp0  44147  corclrcl  44152  relexp0idm  44160  dfrtrcl4  44183  corcltrcl  44184  cotrclrcl  44187  ofsubid  44769  lhe4.4ex1a  44774  dvsconst  44775  dvconstbi  44779  binomcxplemnn0  44794  binomcxplemdvbinom  44798  binomcxplemnotnn0  44801  n0p  45494  climrec  46051  limsup10exlem  46218  dvnmptdivc  46384  dvnmul  46389  stoweidlem55  46501  fourierdlem62  46614  fourierdlem104  46656  fouriersw  46677  ovnval2  46991  hoidmvval  47023  lambert0  47347  tannpoly  47350  sinnpoly  47351  fun2dmnopgexmpl  47744  el1fzopredsuc  47786  cycl3grtrilem  48434  stgrusgra  48447  stgr1  48449  stgrnbgr0  48452  isubgr3stgrlem3  48456  isubgr3stgrlem7  48460  usgrexmpl1lem  48509  usgrexmpl1tri  48513  usgrexmpl2lem  48514  usgrexmpl2nb0  48519  usgrexmpl2nb1  48520  usgrexmpl2nb2  48521  usgrexmpl2nb3  48522  usgrexmpl2nb4  48523  usgrexmpl2nb5  48524  usgrexmpl2trifr  48525  gpgiedgdmellem  48534  gpgvtx0  48541  opgpgvtx  48543  gpgedgvtx0  48549  gpgvtxedg0  48551  gpgvtxedg1  48552  gpgedgiov  48553  gpgedg2ov  48554  gpg5nbgrvtx03starlem1  48556  gpg5nbgrvtx03starlem2  48557  gpg5nbgrvtx03starlem3  48558  gpg5nbgrvtx13starlem1  48559  gpg5nbgrvtx13starlem3  48561  gpg3nbgrvtx0  48564  gpg3nbgrvtx0ALT  48565  gpg3nbgrvtx1  48566  gpgcubic  48567  gpg5nbgr3star  48569  gpg3kgrtriex  48577  gpgprismgr4cycllem2  48584  gpgprismgr4cycllem3  48585  gpgprismgr4cycllem7  48589  gpgprismgr4cycllem9  48591  pgnioedg1  48596  pgnioedg2  48597  pgnioedg3  48598  pgnioedg4  48599  pgnioedg5  48600  pgnbgreunbgrlem1  48601  pgnbgreunbgrlem2lem1  48602  pgnbgreunbgrlem2lem2  48603  pgnbgreunbgrlem2lem3  48604  pgnbgreunbgrlem3  48606  pgnbgreunbgrlem5lem3  48610  pgnbgreunbgrlem5  48611  pgnbgreunbgrlem6  48612  gpg5edgnedg  48618  nn0mnd  48667  zlmodzxzel  48843  zlmodzxz0  48844  zlmodzxzscm  48845  zlmodzxzadd  48846  zlmodzxznm  48985  zlmodzxzldeplem  48986  zlmodzxzldeplem2  48989  blen0  49060  nn0sumshdiglemB  49108  fv1arycl  49125  1arympt1  49126  1arympt1fv  49127  1arymaptf1  49130  1arymaptfo  49131  fv2arycl  49136  2arympt  49137  2arymptfv  49138  2arymaptf1  49141  2arymaptfo  49142  ehl2eudisval0  49213  2sphere0  49238  line2ylem  49239  line2  49240  line2x  49242  line2y  49243  ex-gt  50215  ex-gte  50216  aacllem  50288