Theorem c0ex 11228

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3453  ℂcc 11126  0cc0 11128

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-mulcl 11190  ax-i2m1 11196

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455

This theorem is used by:  0elpr01  11229  ofsubeq0  12243  ofsubge0  12245  elnn0  12534  un0mulcl  12566  fcdmnn0supp  12589  fcdmnn0fsupp  12590  fcdmnn0suppg  12591  fcdmnn0fsuppg  12592  nn0ssz  12642  nn0ind-raph  12725  xaddval  13279  xmulval  13281  ser0f  14123  facnn  14343  fac0  14344  bcval  14372  prhash2ex  14467  wrdexb  14594  s1rn  14670  eqs1  14684  repsw1  14858  cshw1  14897  s1co  14908  funcnvs2  14988  funcnvs3  14989  funcnvs4  14990  wrdlen2i  15017  wrd2pr2op  15018  wrd3tpop  15023  s3rex  15025  wwlktovf1  15034  wrdl3s3  15039  sgnval  15165  sgndm  15173  sgncl  15174  iserge0  15752  sum0  15811  sumz  15812  fsumss  15815  fsumser  15820  isumless  15938  geomulcvg  15969  rpnnen2lem1  16308  ruclem4  16328  ruclem8  16331  ruclem11  16334  0bits  16535  gcdval  16592  lcmval  16688  lcmfpr  16723  lcmfunsnlem2  16736  prmreclem2  17015  prmreclem5  17018  vdwapun  17072  smndex1n0mnd  19030  mgmnsgrpex  19049  odval  19667  odf  19670  gexval  19711  telgsumfz0  20125  telgsum  20127  srgbinom  20376  abvtrivd  21004  pzriprnglem4  21703  pzriprnglem5  21704  pzriprnglem7  21706  pzriprnglem9  21708  pzriprnglem10  21709  snifpsrbag  22141  psrbaglesupp  22143  psrbaglefi  22147  mplcoe5  22262  mplbas2  22264  ltbwe  22266  psrbag0  22284  psrbagev1  22299  mhpmulcl  22383  psdmplcl  22396  psdmvr  22403  cply1coe0bi  22533  m2cpminvid2lem  22985  pmatcollpw3fi1lem1  23017  pmatcollpw3fi1lem2  23018  pmatcollpw3fi1  23019  idpm2idmp  23032  prdsdsf  24599  prdsxmetlem  24600  prdsmet  24602  imasdsf1olem  24605  prdsbl  24723  xrge0gsumle  25066  xrge0tsms  25067  xrhmeo  25180  pcopt  25256  pcopt2  25257  pcoass  25258  rrxcph  25626  rrx0el  25632  rrxbasefi  25644  ovoliunnul  25741  ovolicc1  25750  vitalilem5  25846  mbfpos  25885  0pval  25905  0pledm  25907  i1f1lem  25923  itg11  25925  itg1addlem3  25932  itg1addlem4  25933  i1fres  25939  itg1climres  25948  mbfi1fseqlem4  25952  mbfi1fseqlem6  25954  mbfi1flimlem  25956  mbfi1flim  25957  xrge0f  25965  itg2ge0  25969  itg2uba  25977  itg2splitlem  25982  itg2monolem1  25984  itg2gt0  25994  itg2cnlem1  25995  ibl0  26021  iblcnlem1  26022  i1fibl  26042  itgeqa  26048  itgcn  26079  dvcmul  26178  dvcmulf  26179  dvexp3  26212  dvef  26214  rolle  26224  dveq0  26234  dv11cn  26235  tdeglem4  26292  elply2  26428  elplyd  26434  ply1term  26436  ply0  26440  plyeq0  26444  plypf1  26445  plymullem  26449  dgrlt  26499  plymul0or  26515  plymul02  26517  plymulidp  26519  dvply1  26521  plydivlem4  26533  elqaalem2  26559  iaaOLD  26568  aareccl  26569  aannenlem2  26572  tayl0  26605  taylpfval  26608  dvtaylp  26613  pserdvlem2  26671  abelthlem9  26683  logtayl  26905  cxplogb  27031  leibpilem2  27186  leibpi  27187  jensenlem2  27232  jensen  27233  amgmlem  27234  amgm  27235  igamval  27291  vmaval  27357  vmaf  27363  muval  27376  dchrelbas2  27481  dchrinvcl  27497  dchrptlem2  27509  lgseisenlem4  27622  addsqnreup  27687  pntrlog2bndlem4  27824  pntrlog2bndlem5  27825  padicval  27861  padicabv  27874  ostth1  27877  elcgrabasi  29262  axlowdimlem8  29414  axlowdimlem9  29415  axlowdimlem10  29416  axlowdimlem11  29417  axlowdimlem12  29418  axlowdimlem13  29419  axlowdimlem17  29423  uspgr1ewop  29716  usgr2v1e2w  29720  umgr2v2eedg  29992  umgr2v2e  29993  umgr2v2evd2  29995  wlkl1loop  30105  2wlklem  30133  usgr2trlncl  30233  2wlkdlem4  30404  2wlkdlem5  30405  2pthdlem1  30406  2wlkdlem10  30411  usgrwwlks2on  30434  umgrwwlks2on  30435  rusgrnumwwlkl1  30447  clwwlkn2  30522  0spth  30604  1wlkdlem4  30618  wlk2v2elem1  30643  3wlkdlem4  30650  3wlkdlem5  30651  3pthdlem1  30652  3wlkdlem10  30657  upgr3v3e3cycl  30668  upgr4cycl4dv4e  30673  eulerpathpr  30728  konigsberglem4  30743  konigsberglem5  30744  wlkl0  30855  occllem  31792  0cnfn  32469  0lnfn  32474  nmfn0  32476  nmcexi  32515  nlelchi  32550  fprodex01  33303  indsupp  33321  indfsd  33322  indfsid  33323  gsummulsubdishift1  33516  gsummulsubdishift2s  33519  xrge0tsmsd  33521  cyc2fv1  33569  cyc3evpm  33598  sgnsval  33609  sgnsf  33610  elrgspnlem1  33690  elrgspnlem4  33693  gsumind  33793  0mplrim  34032  selvply1rhmlema  34036  selvply1rhmlemb  34037  selvply1rhmlem1  34038  selvply1rhmlem2  34039  selvply1rhmlem4  34041  selvply1rhm0  34044  extvfvvcl  34053  extvfvcl  34054  esplyfval0  34082  esplysply  34089  esplyind  34093  vieta  34098  constrextdg2lem  34266  xrge0iif1  34456  xrge0mulc1cn  34459  gsumesum  34577  esumpfinval  34593  esumpfinvalf  34594  ddeval1  34753  ddeval0  34754  ddemeas  34755  eulerpartlemt  34890  coinfliprv  35002  signsw0glem  35069  signsw0g  35072  signswmnd  35073  signswrid  35074  prodfzo03  35119  circlevma  35158  circlemethhgt  35159  hgt750lemg  35170  hgt750lemb  35172  hgt750lema  35173  hgt750leme  35174  tgoldbachgtde  35176  tgoldbachgt  35179  cvmliftlem4  35875  cvmliftlem5  35876  poimirlem1  38378  poimirlem2  38379  poimirlem3  38380  poimirlem4  38381  poimirlem5  38382  poimirlem6  38383  poimirlem7  38384  poimirlem11  38388  poimirlem12  38389  poimirlem16  38393  poimirlem17  38394  poimirlem19  38396  poimirlem20  38397  poimirlem22  38399  poimirlem23  38400  poimirlem24  38401  poimirlem25  38402  poimirlem28  38405  poimirlem29  38406  poimirlem31  38408  poimirlem32  38409  poimir  38410  broucube  38411  mblfinlem2  38415  mblfinlem3  38416  ismblfin  38418  itg2addnclem  38428  itg2addnclem3  38430  itg2addnc  38431  ftc1anclem3  38452  ftc1anclem5  38454  ftc1anclem7  38456  ftc1anclem8  38457  ftc1anc  38458  dvacos  38462  prdsbnd  38551  heiborlem10  38578  renegclALT  39844  aks4d1p1p4  42945  aks6d1c7lem1  43054  0prjspnlem  43477  0prjspnrel  43481  diophrw  43612  monotoddzzfi  43791  zindbi  43795  mncn0  43988  aaitgo  44011  flcidc  44019  dfrcl4  44524  iunrelexp0  44550  corclrcl  44555  relexp0idm  44563  dfrtrcl4  44586  corcltrcl  44587  cotrclrcl  44590  ofsubid  45156  lhe4.4ex1a  45161  dvsconst  45162  dvconstbi  45166  binomcxplemnn0  45181  binomcxplemdvbinom  45185  binomcxplemnotnn0  45188  n0p  45887  climrec  46441  limsup10exlem  46608  dvnmptdivc  46774  dvnmul  46779  stoweidlem55  46891  fourierdlem62  47004  fourierdlem104  47046  fouriersw  47067  ovnval2  47381  hoidmvval  47413  lambert0  47763  tannpoly  47766  sinnpoly  47767  fun2dmnopgexmpl  48180  el1fzopredsuc  48222  cycl3grtrilem  48870  stgrusgra  48883  stgrnbgr0  48888  isubgr3stgrlem3  48892  isubgr3stgrlem7  48896  usgrexmpl1lem  48945  usgrexmpl1tri  48949  usgrexmpl2lem  48950  usgrexmpl2nb0  48955  usgrexmpl2nb1  48956  usgrexmpl2nb2  48957  usgrexmpl2nb3  48958  usgrexmpl2nb4  48959  usgrexmpl2nb5  48960  usgrexmpl2trifr  48961  opgpgvtx  48979  gpgedgvtx0  48985  gpgvtxedg0  48987  gpgvtxedg1  48988  gpgedgiov  48989  gpgedg2ov  48990  gpg5nbgrvtx03starlem1  48992  gpg5nbgrvtx03starlem2  48993  gpg5nbgrvtx03starlem3  48994  gpg5nbgrvtx13starlem1  48995  gpg5nbgrvtx13starlem3  48997  gpg3nbgrvtx0  49000  gpg3nbgrvtx0ALT  49001  gpg3nbgrvtx1  49002  gpgcubic  49003  gpg5nbgr3star  49005  gpg3kgrtriex  49013  gpgprismgr4cycllem2  49020  gpgprismgr4cycllem7  49025  pgnioedg1  49032  pgnioedg2  49033  pgnioedg3  49034  pgnioedg4  49035  pgnioedg5  49036  pgnbgreunbgrlem1  49037  pgnbgreunbgrlem2lem1  49038  pgnbgreunbgrlem2lem2  49039  pgnbgreunbgrlem2lem3  49040  pgnbgreunbgrlem3  49042  pgnbgreunbgrlem5lem3  49046  pgnbgreunbgrlem5  49047  pgnbgreunbgrlem6  49048  gpg5edgnedg  49054  nn0mnd  49102  zlmodzxzel  49293  zlmodzxz0  49294  zlmodzxzscm  49295  zlmodzxzadd  49296  zlmodzxznm  49435  zlmodzxzldeplem  49436  zlmodzxzldeplem2  49439  blen0  49510  nn0sumshdiglemB  49558  fv1arycl  49575  1arympt1  49576  1arympt1fv  49577  1arymaptf1  49580  1arymaptfo  49581  fv2arycl  49586  2arymptfv  49588  2arymaptf1  49591  2arymaptfo  49592  ehl2eudisval0  49663  2sphere0  49688  line2ylem  49689  line2  49690  line2x  49692  line2y  49693  ex-gt  50662  ex-gte  50663  aacllem  50780