Theorem c0ex 11170

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

Syntax hints:   ∈ wcel 2141  Vcvv 3453  ℂcc 11068  0cc0 11070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-1cn 11128  ax-icn 11129  ax-addcl 11130  ax-mulcl 11132  ax-i2m1 11138

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455

This theorem is referenced by:  0elpr01  11171  ofsubeq0  12189  ofsubge0  12191  elnn0  12480  un0mulcl  12512  fcdmnn0supp  12535  fcdmnn0fsupp  12536  fcdmnn0suppg  12537  fcdmnn0fsuppg  12538  nn0ssz  12588  nn0ind-raph  12670  xaddval  13223  xmulval  13225  ser0f  14065  facnn  14285  fac0  14286  bcval  14314  prhash2ex  14409  wrdexb  14535  s1rn  14610  eqs1  14623  repsw1  14793  cshw1  14832  s1co  14843  funcnvs2  14923  funcnvs3  14924  funcnvs4  14925  wrdlen2i  14952  wrd2pr2op  14953  wrd3tpop  14958  wwlktovf1  14967  wrdl3s3  14972  sgnval  15098  iserge0  15671  sum0  15731  sumz  15732  fsumss  15735  fsumser  15740  isumless  15858  geomulcvg  15889  rpnnen2lem1  16229  ruclem4  16249  ruclem8  16252  ruclem11  16255  0bits  16456  gcdval  16513  lcmval  16609  lcmfpr  16644  lcmfunsnlem2  16657  prmreclem2  16936  prmreclem5  16939  vdwapun  16993  smndex1n0mnd  18932  mgmnsgrpex  18951  odval  19557  odf  19560  gexval  19601  telgsumfz0  20015  telgsum  20017  srgbinom  20260  abvtrivd  20861  pzriprnglem4  21516  pzriprnglem5  21517  pzriprnglem7  21519  pzriprnglem9  21521  pzriprnglem10  21522  snifpsrbag  21952  psrbaglesupp  21954  psrbaglefi  21958  mplcoe5  22073  mplbas2  22075  ltbwe  22077  psrbag0  22095  psrbagev1  22110  mhpmulcl  22194  psdmplcl  22207  psdmvr  22214  cply1coe0bi  22345  m2cpminvid2lem  22794  pmatcollpw3fi1lem1  22826  pmatcollpw3fi1lem2  22827  pmatcollpw3fi1  22828  idpm2idmp  22841  prdsdsf  24407  prdsxmetlem  24408  prdsmet  24410  imasdsf1olem  24413  prdsbl  24531  xrge0gsumle  24874  xrge0tsms  24875  xrhmeo  24988  pcopt  25064  pcopt2  25065  pcoass  25066  rrxcph  25434  rrx0el  25440  rrxbasefi  25452  ovoliunnul  25549  ovolicc1  25558  vitalilem5  25654  mbfpos  25693  0pval  25713  0pledm  25715  i1f1lem  25731  i1f1  25732  itg11  25733  itg1addlem3  25740  itg1addlem4  25741  i1fres  25747  itg1climres  25756  mbfi1fseqlem4  25760  mbfi1fseqlem6  25762  mbfi1flimlem  25764  mbfi1flim  25765  xrge0f  25773  itg2ge0  25777  itg2uba  25785  itg2splitlem  25790  itg2monolem1  25792  itg2gt0  25802  itg2cnlem1  25803  ibl0  25829  iblcnlem1  25830  i1fibl  25850  itgeqa  25856  itgcn  25887  dvcmul  25986  dvcmulf  25987  dvexp3  26020  dvef  26022  rolle  26032  dveq0  26042  dv11cn  26043  tdeglem4  26100  elply2  26236  elplyd  26242  ply1term  26244  ply0  26248  plyeq0  26251  plypf1  26252  plymullem  26256  dgrlt  26306  plymul0or  26322  dvply1  26325  plydivlem4  26337  elqaalem2  26361  iaa  26366  aareccl  26367  aannenlem2  26370  tayl0  26402  taylpfval  26405  dvtaylp  26410  pserdvlem2  26468  abelthlem9  26480  logtayl  26702  cxplogb  26828  leibpilem2  26983  leibpi  26984  jensenlem2  27029  jensen  27030  amgmlem  27031  amgm  27032  igamval  27088  vmaval  27154  vmaf  27160  muval  27173  dchrelbas2  27278  dchrinvcl  27294  dchrptlem2  27306  lgseisenlem4  27419  addsqnreup  27484  pntrlog2bndlem4  27621  pntrlog2bndlem5  27622  padicval  27658  padicabv  27671  ostth1  27674  axlowdimlem8  29096  axlowdimlem9  29097  axlowdimlem10  29098  axlowdimlem11  29099  axlowdimlem12  29100  axlowdimlem13  29101  axlowdimlem17  29105  uspgr1ewop  29395  usgr2v1e2w  29399  umgr2v2eedg  29671  umgr2v2e  29672  umgr2v2evd2  29674  wlkl1loop  29784  2wlklem  29812  usgr2trlncl  29906  2wlkdlem4  30074  2wlkdlem5  30075  2pthdlem1  30076  2wlkdlem10  30081  usgrwwlks2on  30104  umgrwwlks2on  30105  rusgrnumwwlkl1  30117  clwwlkn2  30192  0spth  30274  1wlkdlem4  30288  wlk2v2elem1  30303  3wlkdlem4  30310  3wlkdlem5  30311  3pthdlem1  30312  3wlkdlem10  30317  upgr3v3e3cycl  30328  upgr4cycl4dv4e  30333  eulerpathpr  30388  konigsberglem4  30403  konigsberglem5  30404  wlkl0  30515  occllem  31452  0cnfn  32129  0lnfn  32134  nmfn0  32136  nmcexi  32175  nlelchi  32210  fprodex01  32977  sgncl  32983  indsupp  33006  indfsd  33007  indfsid  33008  s2rnOLD  33083  s3rnOLD  33085  gsummulsubdishift1  33209  gsummulsubdishift2s  33212  xrge0tsmsd  33214  cyc2fv1  33262  cyc3fv1  33278  cyc3evpm  33291  sgnsval  33302  sgnsf  33303  elrgspnlem1  33384  elrgspnlem4  33387  gsumind  33492  0mplrim  33772  selvply1rhmlema  33776  selvply1rhmlemb  33777  selvply1rhmlem1  33778  selvply1rhmlem2  33779  selvply1rhmlem4  33781  selvply1rhm0  33784  extvfvvcl  33793  extvfvcl  33794  esplyfval0  33822  esplysply  33829  esplyind  33833  vieta  33838  constr01  34000  constrss  34001  constrextdg2lem  34006  nn0constr  34019  xrge0iif1  34196  xrge0mulc1cn  34199  gsumesum  34317  esumpfinval  34333  esumpfinvalf  34334  ddeval1  34492  ddeval0  34493  ddemeas  34494  eulerpartlemt  34629  coinfliprv  34741  plymul02  34804  plymulx  34806  signsw0glem  34811  signsw0g  34814  signswmnd  34815  signswrid  34816  prodfzo03  34861  circlevma  34900  circlemethhgt  34901  hgt750lemg  34912  hgt750lemb  34914  hgt750lema  34915  hgt750leme  34916  tgoldbachgtde  34918  tgoldbachgt  34921  cvmliftlem4  35602  cvmliftlem5  35603  poimirlem1  38084  poimirlem2  38085  poimirlem3  38086  poimirlem4  38087  poimirlem5  38088  poimirlem6  38089  poimirlem7  38090  poimirlem11  38094  poimirlem12  38095  poimirlem16  38099  poimirlem17  38100  poimirlem19  38102  poimirlem20  38103  poimirlem22  38105  poimirlem23  38106  poimirlem24  38107  poimirlem25  38108  poimirlem28  38111  poimirlem29  38112  poimirlem31  38114  poimirlem32  38115  poimir  38116  broucube  38117  mblfinlem2  38121  mblfinlem3  38122  ismblfin  38124  itg2addnclem  38134  itg2addnclem3  38136  itg2addnc  38137  ftc1anclem3  38158  ftc1anclem5  38160  ftc1anclem7  38162  ftc1anclem8  38163  ftc1anc  38164  dvacos  38168  prdsbnd  38256  heiborlem10  38283  renegclALT  39551  aks4d1p1p4  42652  aks6d1c7lem1  42761  0prjspnlem  43169  0prjspnrel  43173  diophrw  43304  monotoddzzfi  43483  zindbi  43487  mncn0  43680  aaitgo  43703  flcidc  43711  dfrcl4  44216  fvrcllb0d  44233  fvrcllb0da  44234  iunrelexp0  44242  corclrcl  44247  relexp0idm  44255  dfrtrcl4  44278  corcltrcl  44279  cotrclrcl  44282  ofsubid  44864  lhe4.4ex1a  44869  dvsconst  44870  dvconstbi  44874  binomcxplemnn0  44889  binomcxplemdvbinom  44893  binomcxplemnotnn0  44896  n0p  45589  climrec  46143  limsup10exlem  46310  dvnmptdivc  46476  dvnmul  46481  stoweidlem55  46593  fourierdlem62  46706  fourierdlem104  46748  fouriersw  46769  ovnval2  47083  hoidmvval  47115  lambert0  47445  tannpoly  47448  sinnpoly  47449  fun2dmnopgexmpl  47842  el1fzopredsuc  47884  cycl3grtrilem  48532  stgrusgra  48545  stgr1  48547  stgrnbgr0  48550  isubgr3stgrlem3  48554  isubgr3stgrlem7  48558  usgrexmpl1lem  48607  usgrexmpl1tri  48611  usgrexmpl2lem  48612  usgrexmpl2nb0  48617  usgrexmpl2nb1  48618  usgrexmpl2nb2  48619  usgrexmpl2nb3  48620  usgrexmpl2nb4  48621  usgrexmpl2nb5  48622  usgrexmpl2trifr  48623  gpgiedgdmellem  48632  gpgvtx0  48639  opgpgvtx  48641  gpgedgvtx0  48647  gpgvtxedg0  48649  gpgvtxedg1  48650  gpgedgiov  48651  gpgedg2ov  48652  gpg5nbgrvtx03starlem1  48654  gpg5nbgrvtx03starlem2  48655  gpg5nbgrvtx03starlem3  48656  gpg5nbgrvtx13starlem1  48657  gpg5nbgrvtx13starlem3  48659  gpg3nbgrvtx0  48662  gpg3nbgrvtx0ALT  48663  gpg3nbgrvtx1  48664  gpgcubic  48665  gpg5nbgr3star  48667  gpg3kgrtriex  48675  gpgprismgr4cycllem2  48682  gpgprismgr4cycllem3  48683  gpgprismgr4cycllem7  48687  gpgprismgr4cycllem9  48689  pgnioedg1  48694  pgnioedg2  48695  pgnioedg3  48696  pgnioedg4  48697  pgnioedg5  48698  pgnbgreunbgrlem1  48699  pgnbgreunbgrlem2lem1  48700  pgnbgreunbgrlem2lem2  48701  pgnbgreunbgrlem2lem3  48702  pgnbgreunbgrlem3  48704  pgnbgreunbgrlem5lem3  48708  pgnbgreunbgrlem5  48709  pgnbgreunbgrlem6  48710  gpg5edgnedg  48716  nn0mnd  48765  zlmodzxzel  48941  zlmodzxz0  48942  zlmodzxzscm  48943  zlmodzxzadd  48944  zlmodzxznm  49083  zlmodzxzldeplem  49084  zlmodzxzldeplem2  49087  blen0  49158  nn0sumshdiglemB  49206  fv1arycl  49223  1arympt1  49224  1arympt1fv  49225  1arymaptf1  49228  1arymaptfo  49229  fv2arycl  49234  2arympt  49235  2arymptfv  49236  2arymaptf1  49239  2arymaptfo  49240  ehl2eudisval0  49311  2sphere0  49336  line2ylem  49337  line2  49338  line2x  49340  line2y  49341  ex-gt  50313  ex-gte  50314  aacllem  50386