Theorem c0ex 11128

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

Syntax hints:   ∈ wcel 2109  Vcvv 3438  ℂcc 11026  0cc0 11028

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-mulcl 11090  ax-i2m1 11096

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440

This theorem is referenced by:  ofsubeq0  12143  ofsubge0  12145  elnn0  12404  un0mulcl  12436  fcdmnn0supp  12459  fcdmnn0fsupp  12460  fcdmnn0suppg  12461  fcdmnn0fsuppg  12462  nn0ssz  12512  nn0ind-raph  12594  xaddval  13143  xmulval  13145  ser0f  13980  facnn  14200  fac0  14201  bcval  14229  prhash2ex  14324  wrdexb  14450  s1rn  14524  eqs1  14537  repsw1  14707  cshw1  14746  s1co  14758  funcnvs2  14838  funcnvs3  14839  funcnvs4  14840  wrdlen2i  14867  wrd2pr2op  14868  wrd3tpop  14873  wwlktovf1  14882  wrdl3s3  14887  sgnval  15013  iserge0  15586  sum0  15646  sumz  15647  fsumss  15650  fsumser  15655  isumless  15770  geomulcvg  15801  rpnnen2lem1  16141  ruclem4  16161  ruclem8  16164  ruclem11  16167  0bits  16368  gcdval  16425  lcmval  16521  lcmfpr  16556  lcmfunsnlem2  16569  prmreclem2  16847  prmreclem5  16850  vdwapun  16904  smndex1n0mnd  18804  mgmnsgrpex  18823  odval  19431  odf  19434  gexval  19475  telgsumfz0  19889  telgsum  19891  srgbinom  20134  abvtrivd  20735  pzriprnglem4  21409  pzriprnglem5  21410  pzriprnglem7  21412  pzriprnglem9  21414  pzriprnglem10  21415  snifpsrbag  21845  psrbaglesupp  21847  psrbaglefi  21851  mplcoe5  21963  mplbas2  21965  ltbwe  21967  psrbag0  21985  psrbagev1  22000  mhpmulcl  22052  psdmplcl  22065  psdmvr  22072  cply1coe0bi  22205  m2cpminvid2lem  22657  pmatcollpw3fi1lem1  22689  pmatcollpw3fi1lem2  22690  pmatcollpw3fi1  22691  idpm2idmp  22704  prdsdsf  24271  prdsxmetlem  24272  prdsmet  24274  imasdsf1olem  24277  prdsbl  24395  xrge0gsumle  24738  xrge0tsms  24739  xrhmeo  24860  pcopt  24938  pcopt2  24939  pcoass  24940  rrxcph  25308  rrx0el  25314  rrxbasefi  25326  ovoliunnul  25424  ovolicc1  25433  vitalilem5  25529  mbfpos  25568  0pval  25588  0pledm  25590  i1f1lem  25606  i1f1  25607  itg11  25608  itg1addlem3  25615  itg1addlem4  25616  i1fres  25622  itg1climres  25631  mbfi1fseqlem4  25635  mbfi1fseqlem6  25637  mbfi1flimlem  25639  mbfi1flim  25640  xrge0f  25648  itg2ge0  25652  itg2uba  25660  itg2splitlem  25665  itg2monolem1  25667  itg2gt0  25677  itg2cnlem1  25678  ibl0  25704  iblcnlem1  25705  i1fibl  25725  itgeqa  25731  itgcn  25762  dvcmul  25863  dvcmulf  25864  dvexp3  25898  dvef  25900  rolle  25910  dveq0  25921  dv11cn  25922  tdeglem4  25981  elply2  26117  elplyd  26123  ply1term  26125  ply0  26129  plyeq0  26132  plypf1  26133  plymullem  26137  dgrlt  26188  plymul0or  26204  dvply1  26207  plydivlem4  26220  elqaalem2  26244  iaa  26249  aareccl  26250  aannenlem2  26253  tayl0  26285  taylpfval  26288  dvtaylp  26294  pserdvlem2  26354  abelthlem9  26366  logtayl  26585  cxplogb  26712  leibpilem2  26867  leibpi  26868  jensenlem2  26914  jensen  26915  amgmlem  26916  amgm  26917  igamval  26973  vmaval  27039  vmaf  27045  muval  27058  dchrelbas2  27164  dchrinvcl  27180  dchrptlem2  27192  lgseisenlem4  27305  addsqnreup  27370  pntrlog2bndlem4  27507  pntrlog2bndlem5  27508  padicval  27544  padicabv  27557  ostth1  27560  axlowdimlem8  28912  axlowdimlem9  28913  axlowdimlem10  28914  axlowdimlem11  28915  axlowdimlem12  28916  axlowdimlem13  28917  axlowdimlem17  28921  uspgr1ewop  29211  usgr2v1e2w  29215  umgr2v2eedg  29488  umgr2v2e  29489  umgr2v2evd2  29491  wlkl1loop  29601  2wlklem  29629  usgr2trlncl  29723  2wlkdlem4  29891  2wlkdlem5  29892  2pthdlem1  29893  2wlkdlem10  29898  umgrwwlks2on  29920  rusgrnumwwlkl1  29931  clwwlkn2  30006  0spth  30088  1wlkdlem4  30102  wlk2v2elem1  30117  3wlkdlem4  30124  3wlkdlem5  30125  3pthdlem1  30126  3wlkdlem10  30131  upgr3v3e3cycl  30142  upgr4cycl4dv4e  30147  eulerpathpr  30202  konigsberglem4  30217  konigsberglem5  30218  wlkl0  30329  occllem  31265  0cnfn  31942  0lnfn  31947  nmfn0  31949  nmcexi  31988  nlelchi  32023  fprodex01  32783  sgncl  32789  indsupp  32823  s2rnOLD  32898  s3rnOLD  32900  xrge0tsmsd  33028  cyc2fv1  33076  cyc3fv1  33092  cyc3evpm  33105  sgnsval  33116  sgnsf  33117  elrgspnlem1  33192  elrgspnlem4  33195  constr01  33708  constrss  33709  constrconj  33711  constrextdg2lem  33714  nn0constr  33727  xrge0iif1  33904  xrge0mulc1cn  33907  gsumesum  34025  esumpfinval  34041  esumpfinvalf  34042  ddeval1  34200  ddeval0  34201  ddemeas  34202  eulerpartlemt  34338  coinfliprv  34450  plymul02  34513  plymulx  34515  signsw0glem  34520  signsw0g  34523  signswmnd  34524  signswrid  34525  prodfzo03  34570  circlevma  34609  circlemethhgt  34610  hgt750lemg  34621  hgt750lemb  34623  hgt750lema  34624  hgt750leme  34625  tgoldbachgtde  34627  tgoldbachgt  34630  cvmliftlem4  35260  cvmliftlem5  35261  poimirlem1  37600  poimirlem2  37601  poimirlem3  37602  poimirlem4  37603  poimirlem5  37604  poimirlem6  37605  poimirlem7  37606  poimirlem11  37610  poimirlem12  37611  poimirlem16  37615  poimirlem17  37616  poimirlem19  37618  poimirlem20  37619  poimirlem22  37621  poimirlem23  37622  poimirlem24  37623  poimirlem25  37624  poimirlem28  37627  poimirlem29  37628  poimirlem31  37630  poimirlem32  37631  poimir  37632  broucube  37633  mblfinlem2  37637  mblfinlem3  37638  ismblfin  37640  itg2addnclem  37650  itg2addnclem3  37652  itg2addnc  37653  ftc1anclem3  37674  ftc1anclem5  37676  ftc1anclem7  37678  ftc1anclem8  37679  ftc1anc  37680  dvacos  37684  prdsbnd  37772  heiborlem10  37799  renegclALT  38941  aks4d1p1p4  42044  aks6d1c7lem1  42153  0prjspnlem  42596  0prjspnrel  42600  diophrw  42732  monotoddzzfi  42915  zindbi  42919  mncn0  43112  aaitgo  43135  flcidc  43143  dfrcl4  43649  fvrcllb0d  43666  fvrcllb0da  43667  iunrelexp0  43675  corclrcl  43680  relexp0idm  43688  dfrtrcl4  43711  corcltrcl  43712  cotrclrcl  43715  ofsubid  44297  lhe4.4ex1a  44302  dvsconst  44303  dvconstbi  44307  binomcxplemnn0  44322  binomcxplemdvbinom  44326  binomcxplemnotnn0  44329  n0p  45023  climrec  45585  limsup10exlem  45754  dvnmptdivc  45920  dvnmul  45925  stoweidlem55  46037  fourierdlem62  46150  fourierdlem104  46192  fouriersw  46213  ovnval2  46527  hoidmvval  46559  tworepnotupword  46868  lambert0  46872  tannpoly  46875  sinnpoly  46876  fun2dmnopgexmpl  47269  el1fzopredsuc  47310  cycl3grtrilem  47931  stgrusgra  47944  stgr1  47946  stgrnbgr0  47949  isubgr3stgrlem3  47953  isubgr3stgrlem7  47957  usgrexmpl1lem  48006  usgrexmpl1tri  48010  usgrexmpl2lem  48011  usgrexmpl2nb0  48016  usgrexmpl2nb1  48017  usgrexmpl2nb2  48018  usgrexmpl2nb3  48019  usgrexmpl2nb4  48020  usgrexmpl2nb5  48021  usgrexmpl2trifr  48022  gpgiedgdmellem  48031  gpgvtx0  48038  opgpgvtx  48040  gpgedgvtx0  48046  gpgvtxedg0  48048  gpgvtxedg1  48049  gpgedgiov  48050  gpgedg2ov  48051  gpg5nbgrvtx03starlem1  48053  gpg5nbgrvtx03starlem2  48054  gpg5nbgrvtx03starlem3  48055  gpg5nbgrvtx13starlem1  48056  gpg5nbgrvtx13starlem3  48058  gpg3nbgrvtx0  48061  gpg3nbgrvtx0ALT  48062  gpg3nbgrvtx1  48063  gpgcubic  48064  gpg5nbgr3star  48066  gpg3kgrtriex  48074  gpgprismgr4cycllem2  48081  gpgprismgr4cycllem3  48082  gpgprismgr4cycllem7  48086  gpgprismgr4cycllem9  48088  pgnioedg1  48093  pgnioedg2  48094  pgnioedg3  48095  pgnioedg4  48096  pgnioedg5  48097  pgnbgreunbgrlem1  48098  pgnbgreunbgrlem2lem1  48099  pgnbgreunbgrlem2lem2  48100  pgnbgreunbgrlem2lem3  48101  pgnbgreunbgrlem3  48103  pgnbgreunbgrlem5lem3  48107  pgnbgreunbgrlem5  48108  pgnbgreunbgrlem6  48109  gpg5edgnedg  48115  nn0mnd  48164  zlmodzxzel  48340  zlmodzxz0  48341  zlmodzxzscm  48342  zlmodzxzadd  48343  zlmodzxznm  48483  zlmodzxzldeplem  48484  zlmodzxzldeplem2  48487  blen0  48558  nn0sumshdiglemB  48606  fv1arycl  48623  1arympt1  48624  1arympt1fv  48625  1arymaptf1  48628  1arymaptfo  48629  fv2arycl  48634  2arympt  48635  2arymptfv  48636  2arymaptf1  48639  2arymaptfo  48640  ehl2eudisval0  48711  2sphere0  48736  line2ylem  48737  line2  48738  line2x  48740  line2y  48741  ex-gt  49714  ex-gte  49715  aacllem  49787