Theorem c0ex 11255

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

Syntax hints:   ∈ wcel 2108  Vcvv 3480  ℂcc 11153  0cc0 11155

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-mulcl 11217  ax-i2m1 11223

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482

This theorem is referenced by:  ofsubeq0  12263  ofsubge0  12265  elnn0  12528  un0mulcl  12560  fcdmnn0supp  12583  fcdmnn0fsupp  12584  fcdmnn0suppg  12585  fcdmnn0fsuppg  12586  nn0ssz  12636  nn0ind-raph  12718  xaddval  13265  xmulval  13267  ser0f  14096  facnn  14314  fac0  14315  bcval  14343  prhash2ex  14438  wrdexb  14563  s1rn  14637  eqs1  14650  repsw1  14821  cshw1  14860  s1co  14872  funcnvs2  14952  funcnvs3  14953  funcnvs4  14954  wrdlen2i  14981  wrd2pr2op  14982  wrd3tpop  14987  wwlktovf1  14996  wrdl3s3  15001  sgnval  15127  iserge0  15697  sum0  15757  sumz  15758  fsumss  15761  fsumser  15766  isumless  15881  geomulcvg  15912  rpnnen2lem1  16250  ruclem4  16270  ruclem8  16273  ruclem11  16276  0bits  16476  gcdval  16533  lcmval  16629  lcmfpr  16664  lcmfunsnlem2  16677  prmreclem2  16955  prmreclem5  16958  vdwapun  17012  smndex1n0mnd  18925  mgmnsgrpex  18944  odval  19552  odf  19555  gexval  19596  telgsumfz0  20010  telgsum  20012  srgbinom  20228  abvtrivd  20833  pzriprnglem4  21495  pzriprnglem5  21496  pzriprnglem7  21498  pzriprnglem9  21500  pzriprnglem10  21501  snifpsrbag  21940  psrbaglesupp  21942  psrbaglefi  21946  mplcoe5  22058  mplbas2  22060  ltbwe  22062  psrbag0  22086  psrbagev1  22101  mhpmulcl  22153  psdmplcl  22166  psdmvr  22173  cply1coe0bi  22306  m2cpminvid2lem  22760  pmatcollpw3fi1lem1  22792  pmatcollpw3fi1lem2  22793  pmatcollpw3fi1  22794  idpm2idmp  22807  prdsdsf  24377  prdsxmetlem  24378  prdsmet  24380  imasdsf1olem  24383  prdsbl  24504  xrge0gsumle  24855  xrge0tsms  24856  xrhmeo  24977  pcopt  25055  pcopt2  25056  pcoass  25057  rrxcph  25426  rrx0el  25432  rrxbasefi  25444  ovoliunnul  25542  ovolicc1  25551  vitalilem5  25647  mbfpos  25686  0pval  25706  0pledm  25708  i1f1lem  25724  i1f1  25725  itg11  25726  itg1addlem3  25733  itg1addlem4  25734  i1fres  25740  itg1climres  25749  mbfi1fseqlem4  25753  mbfi1fseqlem6  25755  mbfi1flimlem  25757  mbfi1flim  25758  xrge0f  25766  itg2ge0  25770  itg2uba  25778  itg2splitlem  25783  itg2monolem1  25785  itg2gt0  25795  itg2cnlem1  25796  ibl0  25822  iblcnlem1  25823  i1fibl  25843  itgeqa  25849  itgcn  25880  dvcmul  25981  dvcmulf  25982  dvexp3  26016  dvef  26018  rolle  26028  dveq0  26039  dv11cn  26040  tdeglem4  26099  elply2  26235  elplyd  26241  ply1term  26243  ply0  26247  plyeq0  26250  plypf1  26251  plymullem  26255  dgrlt  26306  plymul0or  26322  dvply1  26325  plydivlem4  26338  elqaalem2  26362  iaa  26367  aareccl  26368  aannenlem2  26371  tayl0  26403  taylpfval  26406  dvtaylp  26412  pserdvlem2  26472  abelthlem9  26484  logtayl  26702  cxplogb  26829  leibpilem2  26984  leibpi  26985  jensenlem2  27031  jensen  27032  amgmlem  27033  amgm  27034  igamval  27090  vmaval  27156  vmaf  27162  muval  27175  dchrelbas2  27281  dchrinvcl  27297  dchrptlem2  27309  lgseisenlem4  27422  addsqnreup  27487  pntrlog2bndlem4  27624  pntrlog2bndlem5  27625  padicval  27661  padicabv  27674  ostth1  27677  axlowdimlem8  28964  axlowdimlem9  28965  axlowdimlem10  28966  axlowdimlem11  28967  axlowdimlem12  28968  axlowdimlem13  28969  axlowdimlem17  28973  uspgr1ewop  29265  usgr2v1e2w  29269  umgr2v2eedg  29542  umgr2v2e  29543  umgr2v2evd2  29545  wlkl1loop  29656  2wlklem  29685  usgr2trlncl  29780  2wlkdlem4  29948  2wlkdlem5  29949  2pthdlem1  29950  2wlkdlem10  29955  umgrwwlks2on  29977  rusgrnumwwlkl1  29988  clwwlkn2  30063  0spth  30145  1wlkdlem4  30159  wlk2v2elem1  30174  3wlkdlem4  30181  3wlkdlem5  30182  3pthdlem1  30183  3wlkdlem10  30188  upgr3v3e3cycl  30199  upgr4cycl4dv4e  30204  eulerpathpr  30259  konigsberglem4  30274  konigsberglem5  30275  wlkl0  30386  occllem  31322  0cnfn  31999  0lnfn  32004  nmfn0  32006  nmcexi  32045  nlelchi  32080  fprodex01  32827  indsupp  32852  s2rnOLD  32928  s3rnOLD  32930  xrge0tsmsd  33065  cyc2fv1  33141  cyc3fv1  33157  cyc3evpm  33170  sgnsval  33181  sgnsf  33182  elrgspnlem1  33246  elrgspnlem4  33249  constr01  33783  constrss  33784  constrconj  33786  constrextdg2lem  33789  xrge0iif1  33937  xrge0mulc1cn  33940  gsumesum  34060  esumpfinval  34076  esumpfinvalf  34077  ddeval1  34235  ddeval0  34236  ddemeas  34237  eulerpartlemt  34373  coinfliprv  34485  sgncl  34541  plymul02  34561  plymulx  34563  signsw0glem  34568  signsw0g  34571  signswmnd  34572  signswrid  34573  prodfzo03  34618  circlevma  34657  circlemethhgt  34658  hgt750lemg  34669  hgt750lemb  34671  hgt750lema  34672  hgt750leme  34673  tgoldbachgtde  34675  tgoldbachgt  34678  cvmliftlem4  35293  cvmliftlem5  35294  poimirlem1  37628  poimirlem2  37629  poimirlem3  37630  poimirlem4  37631  poimirlem5  37632  poimirlem6  37633  poimirlem7  37634  poimirlem11  37638  poimirlem12  37639  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem22  37649  poimirlem23  37650  poimirlem24  37651  poimirlem25  37652  poimirlem28  37655  poimirlem29  37656  poimirlem31  37658  poimirlem32  37659  poimir  37660  broucube  37661  mblfinlem2  37665  mblfinlem3  37666  ismblfin  37668  itg2addnclem  37678  itg2addnclem3  37680  itg2addnc  37681  ftc1anclem3  37702  ftc1anclem5  37704  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708  dvacos  37712  prdsbnd  37800  heiborlem10  37827  renegclALT  38964  aks4d1p1p4  42072  aks6d1c7lem1  42181  0prjspnlem  42633  0prjspnrel  42637  diophrw  42770  monotoddzzfi  42954  zindbi  42958  mncn0  43151  aaitgo  43174  flcidc  43182  dfrcl4  43689  fvrcllb0d  43706  fvrcllb0da  43707  iunrelexp0  43715  corclrcl  43720  relexp0idm  43728  dfrtrcl4  43751  corcltrcl  43752  cotrclrcl  43755  ofsubid  44343  lhe4.4ex1a  44348  dvsconst  44349  dvconstbi  44353  binomcxplemnn0  44368  binomcxplemdvbinom  44372  binomcxplemnotnn0  44375  n0p  45050  climrec  45618  limsup10exlem  45787  dvnmptdivc  45953  dvnmul  45958  stoweidlem55  46070  fourierdlem62  46183  fourierdlem104  46225  fouriersw  46246  ovnval2  46560  hoidmvval  46592  tworepnotupword  46901  fun2dmnopgexmpl  47296  el1fzopredsuc  47337  cycl3grtrilem  47913  stgrusgra  47926  stgr1  47928  stgrnbgr0  47931  isubgr3stgrlem3  47935  isubgr3stgrlem7  47939  usgrexmpl1lem  47980  usgrexmpl1tri  47984  usgrexmpl2lem  47985  usgrexmpl2nb0  47990  usgrexmpl2nb1  47991  usgrexmpl2nb2  47992  usgrexmpl2nb3  47993  usgrexmpl2nb4  47994  usgrexmpl2nb5  47995  usgrexmpl2trifr  47996  gpgedgel  48007  gpgvtx0  48008  opgpgvtx  48010  gpgedgvtx0  48019  gpgvtxedg0  48021  gpgvtxedg1  48022  gpg5nbgrvtx03starlem1  48024  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx03starlem3  48026  gpg5nbgrvtx13starlem1  48027  gpg5nbgrvtx13starlem3  48029  gpg3nbgrvtx0  48032  gpg3nbgrvtx0ALT  48033  gpg3nbgrvtx1  48034  gpgcubic  48035  gpg5nbgr3star  48037  gpg3kgrtriex  48045  nn0mnd  48095  zlmodzxzel  48271  zlmodzxz0  48272  zlmodzxzscm  48273  zlmodzxzadd  48274  zlmodzxznm  48414  zlmodzxzldeplem  48415  zlmodzxzldeplem2  48418  blen0  48493  nn0sumshdiglemB  48541  fv1arycl  48558  1arympt1  48559  1arympt1fv  48560  1arymaptf1  48563  1arymaptfo  48564  fv2arycl  48569  2arympt  48570  2arymptfv  48571  2arymaptf1  48574  2arymaptfo  48575  ehl2eudisval0  48646  2sphere0  48671  line2ylem  48672  line2  48673  line2x  48675  line2y  48676  ex-gt  49247  ex-gte  49248  aacllem  49320