Theorem c0ex 11281

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451  ℂcc 11179  0cc0 11181

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 2733  ax-1cn 11239  ax-icn 11240  ax-addcl 11241  ax-mulcl 11243  ax-i2m1 11249

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453

This theorem is used by:  0elpr01  11282  ofsubeq0  12298  ofsubge0  12300  elnn0  12589  un0mulcl  12621  fcdmnn0supp  12644  fcdmnn0fsupp  12645  fcdmnn0suppg  12646  fcdmnn0fsuppg  12647  nn0ssz  12697  nn0ind-raph  12780  xaddval  13334  xmulval  13336  ser0f  14178  facnn  14399  fac0  14400  bcval  14428  prhash2ex  14523  wrdexb  14650  s1rn  14726  eqs1  14740  repsw1  14914  cshw1  14953  s1co  14964  funcnvs2  15044  funcnvs3  15045  funcnvs4  15046  wrdlen2i  15073  wrd2pr2op  15074  wrd3tpop  15079  s3rex  15081  wwlktovf1  15090  wrdl3s3  15095  sgnval  15221  sgndm  15229  sgncl  15230  iserge0  15808  sum0  15867  sumz  15868  fsumss  15871  fsumser  15876  isumless  15994  geomulcvg  16025  rpnnen2lem1  16362  ruclem4  16382  ruclem8  16385  ruclem11  16388  0bits  16589  gcdval  16646  lcmval  16747  lcmfpr  16782  lcmfunsnlem2  16795  prmreclem2  17075  prmreclem5  17078  vdwapun  17132  smndex1n0mnd  19091  mgmnsgrpex  19110  odval  19728  odf  19731  gexval  19772  telgsumfz0  20186  telgsum  20188  srgbinom  20437  abvtrivd  21069  pzriprnglem4  21770  pzriprnglem5  21771  pzriprnglem7  21773  pzriprnglem9  21775  pzriprnglem10  21776  snifpsrbag  22208  psrbaglesupp  22210  psrbaglefi  22214  mplcoe5  22329  mplbas2  22331  ltbwe  22333  psrbag0  22351  psrbagev1  22366  mhpmulcl  22450  psdmplcl  22463  psdmvr  22470  cply1coe0bi  22600  m2cpminvid2lem  23052  pmatcollpw3fi1lem1  23084  pmatcollpw3fi1lem2  23085  pmatcollpw3fi1  23086  idpm2idmp  23099  prdsdsf  24666  prdsxmetlem  24667  prdsmet  24669  imasdsf1olem  24672  prdsbl  24790  xrge0gsumle  25133  xrge0tsms  25134  xrhmeo  25247  pcopt  25323  pcopt2  25324  pcoass  25325  rrxcph  25693  rrx0el  25699  rrxbasefi  25711  ovoliunnul  25808  ovolicc1  25817  vitalilem5  25913  mbfpos  25952  0pval  25972  0pledm  25974  i1f1lem  25990  itg11  25992  itg1addlem3  25999  itg1addlem4  26000  i1fres  26006  itg1climres  26015  mbfi1fseqlem4  26019  mbfi1fseqlem6  26021  mbfi1flimlem  26023  mbfi1flim  26024  xrge0f  26032  itg2ge0  26036  itg2uba  26044  itg2splitlem  26049  itg2monolem1  26051  itg2gt0  26061  itg2cnlem1  26062  ibl0  26087  iblcnlem1  26088  i1fibl  26108  itgeqa  26114  itgcn  26145  dvcmul  26244  dvcmulf  26245  dvexp3  26278  dvef  26280  rolle  26290  dveq0  26300  dv11cn  26301  tdeglem4  26358  elply2  26494  elplyd  26500  ply1term  26502  ply0  26506  plyeq0  26510  plypf1  26511  plymullem  26515  dgrlt  26565  plymul0or  26581  plymul02  26583  plymulidp  26585  dvply1  26587  plydivlem4  26599  elqaalem2  26625  iaaOLD  26634  aareccl  26635  aannenlem2  26638  tayl0  26671  taylpfval  26674  dvtaylp  26679  pserdvlem2  26737  abelthlem9  26749  logtayl  26970  cxplogb  27096  leibpilem2  27251  leibpi  27252  jensenlem2  27297  jensen  27298  amgmlem  27299  amgm  27300  igamval  27356  vmaval  27422  vmaf  27428  muval  27441  dchrelbas2  27546  dchrinvcl  27562  dchrptlem2  27574  lgseisenlem4  27687  addsqnreup  27752  pntrlog2bndlem4  27889  pntrlog2bndlem5  27890  padicval  27926  padicabv  27939  ostth1  27942  elcgrabasi  29357  axlowdimlem8  29509  axlowdimlem9  29510  axlowdimlem10  29511  axlowdimlem11  29512  axlowdimlem12  29513  axlowdimlem13  29514  axlowdimlem17  29518  uspgr1ewop  29811  usgr2v1e2w  29815  umgr2v2eedg  30087  umgr2v2e  30088  umgr2v2evd2  30090  wlkl1loop  30200  2wlklem  30228  usgr2trlncl  30328  2wlkdlem4  30499  2wlkdlem5  30500  2pthdlem1  30501  2wlkdlem10  30506  usgrwwlks2on  30529  umgrwwlks2on  30530  rusgrnumwwlkl1  30542  clwwlkn2  30617  0spth  30699  1wlkdlem4  30713  wlk2v2elem1  30738  3wlkdlem4  30745  3wlkdlem5  30746  3pthdlem1  30747  3wlkdlem10  30752  upgr3v3e3cycl  30763  upgr4cycl4dv4e  30768  eulerpathpr  30823  konigsberglem4  30838  konigsberglem5  30839  wlkl0  30950  occllem  31887  0cnfn  32564  0lnfn  32569  nmfn0  32571  nmcexi  32610  nlelchi  32645  fprodex01  33398  indsupp  33416  indfsd  33417  indfsid  33418  gsummulsubdishift1  33611  gsummulsubdishift2s  33614  xrge0tsmsd  33616  cyc2fv1  33664  cyc3evpm  33693  sgnsval  33704  sgnsf  33705  elrgspnlem1  33785  elrgspnlem4  33788  gsumind  33888  0mplrim  34128  selvply1rhmlema  34132  selvply1rhmlemb  34133  selvply1rhmlem1  34134  selvply1rhmlem2  34135  selvply1rhmlem4  34137  selvply1rhm0  34140  extvfvvcl  34149  extvfvcl  34150  esplyfval0  34178  esplysply  34185  esplyind  34189  vieta  34194  constrextdg2lem  34362  xrge0iif1  34552  xrge0mulc1cn  34555  gsumesum  34673  esumpfinval  34689  esumpfinvalf  34690  ddeval1  34849  ddeval0  34850  ddemeas  34851  eulerpartlemt  34986  coinfliprv  35098  signsw0glem  35165  signsw0g  35168  signswmnd  35169  signswrid  35170  prodfzo03  35215  circlevma  35254  circlemethhgt  35255  hgt750lemg  35266  hgt750lemb  35268  hgt750lema  35269  hgt750leme  35270  tgoldbachgtde  35272  tgoldbachgt  35275  cvmliftlem4  36022  cvmliftlem5  36023  poimirlem1  38507  poimirlem2  38508  poimirlem3  38509  poimirlem4  38510  poimirlem5  38511  poimirlem6  38512  poimirlem7  38513  poimirlem11  38517  poimirlem12  38518  poimirlem16  38522  poimirlem17  38523  poimirlem19  38525  poimirlem20  38526  poimirlem22  38528  poimirlem23  38529  poimirlem24  38530  poimirlem25  38531  poimirlem28  38534  poimirlem29  38535  poimirlem31  38537  poimirlem32  38538  poimir  38539  broucube  38540  mblfinlem2  38544  mblfinlem3  38545  ismblfin  38547  itg2addnclem  38557  itg2addnclem3  38559  itg2addnc  38560  ftc1anclem3  38581  ftc1anclem5  38583  ftc1anclem7  38585  ftc1anclem8  38586  ftc1anc  38587  dvacos  38591  prdsbnd  38695  heiborlem10  38722  renegclALT  39988  aks4d1p1p4  43089  aks6d1c7lem1  43198  0prjspnlem  43613  0prjspnrel  43617  diophrw  43723  monotoddzzfi  43902  zindbi  43906  mncn0  44099  aaitgo  44122  flcidc  44130  dfrcl4  44635  iunrelexp0  44661  corclrcl  44666  relexp0idm  44674  dfrtrcl4  44697  corcltrcl  44698  cotrclrcl  44701  ofsubid  45267  lhe4.4ex1a  45272  dvsconst  45273  dvconstbi  45277  binomcxplemnn0  45292  binomcxplemdvbinom  45296  binomcxplemnotnn0  45299  n0p  46005  climrec  46559  limsup10exlem  46726  dvnmptdivc  46892  dvnmul  46897  stoweidlem55  47009  fourierdlem62  47122  fourierdlem104  47164  fouriersw  47185  ovnval2  47499  hoidmvval  47531  lambert0  47881  tannpoly  47884  sinnpoly  47885  fun2dmnopgexmpl  48298  el1fzopredsuc  48340  cycl3grtrilem  48988  stgrusgra  49001  stgrnbgr0  49006  isubgr3stgrlem3  49010  isubgr3stgrlem7  49014  usgrexmpl1lem  49063  usgrexmpl1tri  49067  usgrexmpl2lem  49068  usgrexmpl2nb0  49073  usgrexmpl2nb1  49074  usgrexmpl2nb2  49075  usgrexmpl2nb3  49076  usgrexmpl2nb4  49077  usgrexmpl2nb5  49078  usgrexmpl2trifr  49079  opgpgvtx  49097  gpgedgvtx0  49103  gpgvtxedg0  49105  gpgvtxedg1  49106  gpgedgiov  49107  gpgedg2ov  49108  gpg5nbgrvtx03starlem1  49110  gpg5nbgrvtx03starlem2  49111  gpg5nbgrvtx03starlem3  49112  gpg5nbgrvtx13starlem1  49113  gpg5nbgrvtx13starlem3  49115  gpg3nbgrvtx0  49118  gpg3nbgrvtx0ALT  49119  gpg3nbgrvtx1  49120  gpgcubic  49121  gpg5nbgr3star  49123  gpg3kgrtriex  49131  gpgprismgr4cycllem2  49138  gpgprismgr4cycllem7  49143  pgnioedg1  49150  pgnioedg2  49151  pgnioedg3  49152  pgnioedg4  49153  pgnioedg5  49154  pgnbgreunbgrlem1  49155  pgnbgreunbgrlem2lem1  49156  pgnbgreunbgrlem2lem2  49157  pgnbgreunbgrlem2lem3  49158  pgnbgreunbgrlem3  49160  pgnbgreunbgrlem5lem3  49164  pgnbgreunbgrlem5  49165  pgnbgreunbgrlem6  49166  gpg5edgnedg  49172  nn0mnd  49220  zlmodzxzel  49411  zlmodzxz0  49412  zlmodzxzscm  49413  zlmodzxzadd  49414  zlmodzxznm  49553  zlmodzxzldeplem  49554  zlmodzxzldeplem2  49557  blen0  49628  nn0sumshdiglemB  49676  fv1arycl  49693  1arympt1  49694  1arympt1fv  49695  1arymaptf1  49698  1arymaptfo  49699  fv2arycl  49704  2arymptfv  49706  2arymaptf1  49709  2arymaptfo  49710  ehl2eudisval0  49781  2sphere0  49806  line2ylem  49807  line2  49808  line2x  49810  line2y  49811  ex-gt  50765  ex-gte  50766  aacllem  50883