Theorem c0ex 10034

Description: 0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)

Assertion

Ref	Expression
c0ex	|- 0 e. _V

Proof of Theorem c0ex

Step	Hyp	Ref	Expression
1		0cn 10032	. 2 |- 0 e. CC
2	1	elexi 3213	1 |- 0 e. _V

Syntax hints:   e. wcel 1990   _Vcvv 3200   CCcc 9934   0cc0 9936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-12 2047  ax-ext 2602  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-mulcl 9998  ax-i2m1 10004

This theorem depends on definitions:  df-bi 197  df-an 386  df-tru 1486  df-ex 1705  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-v 3202

This theorem is referenced by:  ofsubeq0  11017  ofsubge0  11019  elnn0  11294  un0mulcl  11327  frnnn0supp  11349  frnnn0fsupp  11350  nn0ssz  11398  nn0ind-raph  11477  xaddval  12054  xmulval  12056  ser0f  12854  facnn  13062  fac0  13063  bcval  13091  prhash2ex  13187  wrdexb  13316  s1rn  13379  eqs1  13392  repsw1  13530  cshw1  13568  s1co  13579  funcnvs2  13658  funcnvs3  13659  funcnvs4  13660  wrdlen2i  13686  wrd2pr2op  13687  wrd3tpop  13691  wwlktovf1  13700  wrdl3s3  13705  sgnval  13828  iserge0  14391  sum0  14452  sumz  14453  fsumss  14456  fsumser  14461  isumless  14577  geomulcvg  14607  rpnnen2lem1  14943  ruclem4  14963  ruclem8  14966  ruclem11  14969  0bits  15161  gcdval  15218  lcmval  15305  lcmfpr  15340  lcmfunsnlem2  15353  prmreclem2  15621  prmreclem5  15624  vdwapun  15678  mgmnsgrpex  17418  odval  17953  odf  17956  gexval  17993  telgsumfz0  18389  telgsum  18391  srgbinom  18545  abvtrivd  18840  snifpsrbag  19366  psrbaglesupp  19368  psrbagaddcl  19370  psrbaglefi  19372  mplcoe5  19468  mplbas2  19470  ltbwe  19472  psrbag0  19494  psrbagev1  19510  cply1coe0bi  19670  m2cpminvid2lem  20559  pmatcollpw3fi1lem1  20591  pmatcollpw3fi1lem2  20592  pmatcollpw3fi1  20593  idpm2idmp  20606  prdsdsf  22172  prdsxmetlem  22173  prdsmet  22175  imasdsf1olem  22178  prdsbl  22296  xrge0gsumle  22636  xrge0tsms  22637  xrhmeo  22745  pcopt  22822  pcopt2  22823  pcoass  22824  rrxcph  23180  ovoliunnul  23275  ovolicc1  23284  vitalilem5  23381  mbfpos  23418  0pval  23438  0pledm  23440  i1f1lem  23456  i1f1  23457  itg11  23458  itg1addlem3  23465  itg1addlem4  23466  i1fres  23472  itg1climres  23481  mbfi1fseqlem4  23485  mbfi1fseqlem6  23487  mbfi1flimlem  23489  mbfi1flim  23490  xrge0f  23498  itg2ge0  23502  itg2uba  23510  itg2splitlem  23515  itg2monolem1  23517  itg2gt0  23527  itg2cnlem1  23528  ibl0  23553  iblcnlem1  23554  i1fibl  23574  itgeqa  23580  itgcn  23609  dvcmul  23707  dvcmulf  23708  dvexp3  23741  rolle  23753  dveq0  23763  dv11cn  23764  tdeglem4  23820  elply2  23952  elplyd  23958  ply1term  23960  ply0  23964  plyeq0  23967  plypf1  23968  plymullem  23972  dgrlt  24022  plymul0or  24036  dvply1  24039  plydivlem4  24051  elqaalem2  24075  iaa  24080  aareccl  24081  aannenlem2  24084  tayl0  24116  taylpfval  24119  dvtaylp  24124  pserdvlem2  24182  abelthlem9  24194  logtayl  24406  cxplogb  24524  leibpilem2  24668  leibpi  24669  jensenlem2  24714  jensen  24715  amgmlem  24716  amgm  24717  igamval  24773  vmaval  24839  vmaf  24845  muval  24858  dchrelbas2  24962  dchrinvcl  24978  dchrptlem2  24990  lgseisenlem4  25103  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  padicval  25306  padicabv  25319  ostth1  25322  axlowdimlem8  25829  axlowdimlem9  25830  axlowdimlem10  25831  axlowdimlem11  25832  axlowdimlem12  25833  axlowdimlem13  25834  axlowdimlem17  25838  uspgr1ewop  26140  usgr2v1e2w  26144  umgr2v2eedg  26420  umgr2v2e  26421  umgr2v2evd2  26423  wlkl1loop  26534  2wlklem  26563  usgr2trlncl  26656  2wlkdlem4  26824  2wlkdlem5  26825  2pthdlem1  26826  2wlkdlem10  26831  umgrwwlks2on  26850  rusgrnumwwlkl1  26863  clwwlksn2  26910  0spth  26987  1wlkdlem4  27000  wlk2v2elem1  27015  3wlkdlem4  27022  3wlkdlem5  27023  3pthdlem1  27024  3wlkdlem10  27029  upgr3v3e3cycl  27040  upgr4cycl4dv4e  27045  eulerpathpr  27100  konigsberglem4  27117  konigsberglem5  27118  occllem  28162  0cnfn  28839  0lnfn  28844  nmfn0  28846  nmcexi  28885  nlelchi  28920  fprodex01  29571  sgnsval  29728  sgnsf  29729  xrge0tsmsd  29785  xrge0iif1  29984  xrge0mulc1cn  29987  gsumesum  30121  esumpfinval  30137  esumpfinvalf  30138  ddeval1  30297  ddeval0  30298  ddemeas  30299  eulerpartlemt  30433  coinfliprv  30544  sgncl  30600  plymul02  30623  plymulx  30625  signsw0glem  30630  signsw0g  30633  signswmnd  30634  signswrid  30635  signstfvn  30646  prodfzo03  30681  circlevma  30720  circlemethhgt  30721  hgt750lemg  30732  hgt750lemb  30734  hgt750lema  30735  hgt750leme  30736  tgoldbachgtde  30738  tgoldbachgt  30741  cvmliftlem4  31270  cvmliftlem5  31271  poimirlem1  33410  poimirlem2  33411  poimirlem3  33412  poimirlem4  33413  poimirlem5  33414  poimirlem6  33415  poimirlem7  33416  poimirlem11  33420  poimirlem12  33421  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem22  33431  poimirlem23  33432  poimirlem24  33433  poimirlem25  33434  poimirlem28  33437  poimirlem29  33438  poimirlem31  33440  poimirlem32  33441  poimir  33442  broucube  33443  mblfinlem2  33447  mblfinlem3  33448  ismblfin  33450  itg2addnclem  33461  itg2addnclem3  33463  itg2addnc  33464  ftc1anclem3  33487  ftc1anclem5  33489  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  dvacos  33497  prdsbnd  33592  heiborlem10  33619  renegclALT  34249  diophrw  37322  monotoddzzfi  37507  zindbi  37511  mncn0  37709  aaitgo  37732  flcidc  37744  dfrcl4  37968  fvrcllb0d  37985  fvrcllb0da  37986  iunrelexp0  37994  corclrcl  37999  relexp0idm  38007  dfrtrcl4  38030  corcltrcl  38031  cotrclrcl  38034  ofsubid  38523  lhe4.4ex1a  38528  dvsconst  38529  dvconstbi  38533  binomcxplemnn0  38548  binomcxplemdvbinom  38552  binomcxplemnotnn0  38555  n0p  39209  climrec  39835  limsup10exlem  40004  dvnmptdivc  40153  dvnmul  40158  stoweidlem55  40272  fourierdlem62  40385  fourierdlem104  40427  fouriersw  40448  rrxbasefi  40503  ovnval2  40759  hoidmvval  40791  hoidmvlelem1  40809  fun2dmnopgexmpl  41303  el1fzopredsuc  41335  zlmodzxzel  42133  zlmodzxz0  42134  zlmodzxzscm  42135  zlmodzxzadd  42136  zlmodzxznm  42286  zlmodzxzldeplem  42287  zlmodzxzldeplem2  42290  blen0  42366  nn0sumshdiglemB  42414  ex-gt  42469  ex-gte  42470  aacllem  42547