Theorem c0ex 11188

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

Syntax hints:   ∈ wcel 2145  Vcvv 3457  ℂcc 11086  0cc0 11088

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-mulcl 11150  ax-i2m1 11156

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459

This theorem is referenced by:  0elpr01  11189  ofsubeq0  12203  ofsubge0  12205  elnn0  12494  un0mulcl  12526  fcdmnn0supp  12549  fcdmnn0fsupp  12550  fcdmnn0suppg  12551  fcdmnn0fsuppg  12552  nn0ssz  12602  nn0ind-raph  12684  xaddval  13237  xmulval  13239  ser0f  14079  facnn  14299  fac0  14300  bcval  14328  prhash2ex  14423  wrdexb  14550  s1rn  14625  eqs1  14638  repsw1  14808  cshw1  14847  s1co  14858  funcnvs2  14938  funcnvs3  14939  funcnvs4  14940  wrdlen2i  14967  wrd2pr2op  14968  wrd3tpop  14973  wwlktovf1  14982  wrdl3s3  14987  sgnval  15113  sgndm  15121  sgncl  15122  iserge0  15700  sum0  15760  sumz  15761  fsumss  15764  fsumser  15769  isumless  15887  geomulcvg  15918  rpnnen2lem1  16258  ruclem4  16278  ruclem8  16281  ruclem11  16284  0bits  16485  gcdval  16542  lcmval  16638  lcmfpr  16673  lcmfunsnlem2  16686  prmreclem2  16965  prmreclem5  16968  vdwapun  17022  smndex1n0mnd  18962  mgmnsgrpex  18981  odval  19592  odf  19595  gexval  19636  telgsumfz0  20050  telgsum  20052  srgbinom  20301  abvtrivd  20901  pzriprnglem4  21591  pzriprnglem5  21592  pzriprnglem7  21594  pzriprnglem9  21596  pzriprnglem10  21597  snifpsrbag  22027  psrbaglesupp  22029  psrbaglefi  22033  mplcoe5  22148  mplbas2  22150  ltbwe  22152  psrbag0  22170  psrbagev1  22185  mhpmulcl  22269  psdmplcl  22282  psdmvr  22289  cply1coe0bi  22419  m2cpminvid2lem  22868  pmatcollpw3fi1lem1  22900  pmatcollpw3fi1lem2  22901  pmatcollpw3fi1  22902  idpm2idmp  22915  prdsdsf  24481  prdsxmetlem  24482  prdsmet  24484  imasdsf1olem  24487  prdsbl  24605  xrge0gsumle  24948  xrge0tsms  24949  xrhmeo  25062  pcopt  25138  pcopt2  25139  pcoass  25140  rrxcph  25508  rrx0el  25514  rrxbasefi  25526  ovoliunnul  25623  ovolicc1  25632  vitalilem5  25728  mbfpos  25767  0pval  25787  0pledm  25789  i1f1lem  25805  i1f1  25806  itg11  25807  itg1addlem3  25814  itg1addlem4  25815  i1fres  25821  itg1climres  25830  mbfi1fseqlem4  25834  mbfi1fseqlem6  25836  mbfi1flimlem  25838  mbfi1flim  25839  xrge0f  25847  itg2ge0  25851  itg2uba  25859  itg2splitlem  25864  itg2monolem1  25866  itg2gt0  25876  itg2cnlem1  25877  ibl0  25903  iblcnlem1  25904  i1fibl  25924  itgeqa  25930  itgcn  25961  dvcmul  26060  dvcmulf  26061  dvexp3  26094  dvef  26096  rolle  26106  dveq0  26116  dv11cn  26117  tdeglem4  26174  elply2  26310  elplyd  26316  ply1term  26318  ply0  26322  plyeq0  26325  plypf1  26326  plymullem  26330  dgrlt  26380  plymul0or  26396  plymul02  26398  plymulidp  26400  dvply1  26402  plydivlem4  26414  elqaalem2  26438  iaa  26443  aareccl  26444  aannenlem2  26447  tayl0  26479  taylpfval  26482  dvtaylp  26487  pserdvlem2  26545  abelthlem9  26557  logtayl  26779  cxplogb  26905  leibpilem2  27060  leibpi  27061  jensenlem2  27106  jensen  27107  amgmlem  27108  amgm  27109  igamval  27165  vmaval  27231  vmaf  27237  muval  27250  dchrelbas2  27355  dchrinvcl  27371  dchrptlem2  27383  lgseisenlem4  27496  addsqnreup  27561  pntrlog2bndlem4  27698  pntrlog2bndlem5  27699  padicval  27735  padicabv  27748  ostth1  27751  axlowdimlem8  29204  axlowdimlem9  29205  axlowdimlem10  29206  axlowdimlem11  29207  axlowdimlem12  29208  axlowdimlem13  29209  axlowdimlem17  29213  uspgr1ewop  29503  usgr2v1e2w  29507  umgr2v2eedg  29779  umgr2v2e  29780  umgr2v2evd2  29782  wlkl1loop  29892  2wlklem  29920  usgr2trlncl  30014  2wlkdlem4  30182  2wlkdlem5  30183  2pthdlem1  30184  2wlkdlem10  30189  usgrwwlks2on  30212  umgrwwlks2on  30213  rusgrnumwwlkl1  30225  clwwlkn2  30300  0spth  30382  1wlkdlem4  30396  wlk2v2elem1  30411  3wlkdlem4  30418  3wlkdlem5  30419  3pthdlem1  30420  3wlkdlem10  30425  upgr3v3e3cycl  30436  upgr4cycl4dv4e  30441  eulerpathpr  30496  konigsberglem4  30511  konigsberglem5  30512  wlkl0  30623  occllem  31560  0cnfn  32237  0lnfn  32242  nmfn0  32244  nmcexi  32283  nlelchi  32318  fprodex01  33077  indsupp  33095  indfsd  33096  indfsid  33097  s2rnOLD  33172  s3rnOLD  33174  gsummulsubdishift1  33296  gsummulsubdishift2s  33299  xrge0tsmsd  33301  cyc2fv1  33349  cyc3fv1  33365  cyc3evpm  33378  sgnsval  33389  sgnsf  33390  elrgspnlem1  33470  elrgspnlem4  33473  gsumind  33575  0mplrim  33816  selvply1rhmlema  33820  selvply1rhmlemb  33821  selvply1rhmlem1  33822  selvply1rhmlem2  33823  selvply1rhmlem4  33825  selvply1rhm0  33828  extvfvvcl  33837  extvfvcl  33838  esplyfval0  33866  esplysply  33873  esplyind  33877  vieta  33882  constr01  34044  constrss  34045  constrextdg2lem  34050  nn0constr  34063  xrge0iif1  34240  xrge0mulc1cn  34243  gsumesum  34361  esumpfinval  34377  esumpfinvalf  34378  ddeval1  34536  ddeval0  34537  ddemeas  34538  eulerpartlemt  34673  coinfliprv  34785  signsw0glem  34852  signsw0g  34855  signswmnd  34856  signswrid  34857  prodfzo03  34902  circlevma  34941  circlemethhgt  34942  hgt750lemg  34953  hgt750lemb  34955  hgt750lema  34956  hgt750leme  34957  tgoldbachgtde  34959  tgoldbachgt  34962  cvmliftlem4  35646  cvmliftlem5  35647  poimirlem1  38127  poimirlem2  38128  poimirlem3  38129  poimirlem4  38130  poimirlem5  38131  poimirlem6  38132  poimirlem7  38133  poimirlem11  38137  poimirlem12  38138  poimirlem16  38142  poimirlem17  38143  poimirlem19  38145  poimirlem20  38146  poimirlem22  38148  poimirlem23  38149  poimirlem24  38150  poimirlem25  38151  poimirlem28  38154  poimirlem29  38155  poimirlem31  38157  poimirlem32  38158  poimir  38159  broucube  38160  mblfinlem2  38164  mblfinlem3  38165  ismblfin  38167  itg2addnclem  38177  itg2addnclem3  38179  itg2addnc  38180  ftc1anclem3  38201  ftc1anclem5  38203  ftc1anclem7  38205  ftc1anclem8  38206  ftc1anc  38207  dvacos  38211  prdsbnd  38299  heiborlem10  38326  renegclALT  39594  aks4d1p1p4  42695  aks6d1c7lem1  42804  0prjspnlem  43212  0prjspnrel  43216  diophrw  43347  monotoddzzfi  43526  zindbi  43530  mncn0  43723  aaitgo  43746  flcidc  43754  dfrcl4  44259  fvrcllb0d  44276  fvrcllb0da  44277  iunrelexp0  44285  corclrcl  44290  relexp0idm  44298  dfrtrcl4  44321  corcltrcl  44322  cotrclrcl  44325  ofsubid  44893  lhe4.4ex1a  44898  dvsconst  44899  dvconstbi  44903  binomcxplemnn0  44918  binomcxplemdvbinom  44922  binomcxplemnotnn0  44925  n0p  45624  climrec  46178  limsup10exlem  46345  dvnmptdivc  46511  dvnmul  46516  stoweidlem55  46628  fourierdlem62  46741  fourierdlem104  46783  fouriersw  46804  ovnval2  47118  hoidmvval  47150  lambert0  47480  tannpoly  47483  sinnpoly  47484  fun2dmnopgexmpl  47877  el1fzopredsuc  47919  cycl3grtrilem  48567  stgrusgra  48580  stgr1  48582  stgrnbgr0  48585  isubgr3stgrlem3  48589  isubgr3stgrlem7  48593  usgrexmpl1lem  48642  usgrexmpl1tri  48646  usgrexmpl2lem  48647  usgrexmpl2nb0  48652  usgrexmpl2nb1  48653  usgrexmpl2nb2  48654  usgrexmpl2nb3  48655  usgrexmpl2nb4  48656  usgrexmpl2nb5  48657  usgrexmpl2trifr  48658  gpgiedgdmellem  48667  gpgvtx0  48674  opgpgvtx  48676  gpgedgvtx0  48682  gpgvtxedg0  48684  gpgvtxedg1  48685  gpgedgiov  48686  gpgedg2ov  48687  gpg5nbgrvtx03starlem1  48689  gpg5nbgrvtx03starlem2  48690  gpg5nbgrvtx03starlem3  48691  gpg5nbgrvtx13starlem1  48692  gpg5nbgrvtx13starlem3  48694  gpg3nbgrvtx0  48697  gpg3nbgrvtx0ALT  48698  gpg3nbgrvtx1  48699  gpgcubic  48700  gpg5nbgr3star  48702  gpg3kgrtriex  48710  gpgprismgr4cycllem2  48717  gpgprismgr4cycllem3  48718  gpgprismgr4cycllem7  48722  gpgprismgr4cycllem9  48724  pgnioedg1  48729  pgnioedg2  48730  pgnioedg3  48731  pgnioedg4  48732  pgnioedg5  48733  pgnbgreunbgrlem1  48734  pgnbgreunbgrlem2lem1  48735  pgnbgreunbgrlem2lem2  48736  pgnbgreunbgrlem2lem3  48737  pgnbgreunbgrlem3  48739  pgnbgreunbgrlem5lem3  48743  pgnbgreunbgrlem5  48744  pgnbgreunbgrlem6  48745  gpg5edgnedg  48751  nn0mnd  48800  zlmodzxzel  48987  zlmodzxz0  48988  zlmodzxzscm  48989  zlmodzxzadd  48990  zlmodzxznm  49129  zlmodzxzldeplem  49130  zlmodzxzldeplem2  49133  blen0  49204  nn0sumshdiglemB  49252  fv1arycl  49269  1arympt1  49270  1arympt1fv  49271  1arymaptf1  49274  1arymaptfo  49275  fv2arycl  49280  2arympt  49281  2arymptfv  49282  2arymaptf1  49285  2arymaptfo  49286  ehl2eudisval0  49357  2sphere0  49382  line2ylem  49383  line2  49384  line2x  49386  line2y  49387  ex-gt  50358  ex-gte  50359  aacllem  50431