MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  c0ex Structured version   Visualization version   Unicode version

Theorem c0ex 9655
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
StepHypRef Expression
1 0cn 9653 . 2  |-  0  e.  CC
21elexi 3041 1  |-  0  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1904   _Vcvv 3031   CCcc 9555   0cc0 9557
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-12 1950  ax-ext 2451  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-mulcl 9619  ax-i2m1 9625
This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-v 3033
This theorem is referenced by:  ofsubeq0  10628  ofsubge0  10630  elnn0  10895  un0mulcl  10928  frnnn0supp  10947  frnnn0fsupp  10948  nn0ssz  10982  nn0ind-raph  11058  xaddval  11539  xmulval  11541  ser0f  12304  facnn  12499  fac0  12500  bcval  12527  prhash2ex  12614  snopiswrd  12728  wrdexb  12730  s1rn  12791  eqs1  12803  repsw1  12940  cshw1  12978  s1co  12989  funcnvs2  13067  funcnvs3  13068  funcnvs4  13069  wrdlen2i  13093  wrd2pr2op  13094  wrd3tpop  13098  wwlktovf1  13107  sgnval  13228  iserge0  13801  sum0  13864  sumz  13865  fsumss  13868  fsumser  13873  isumless  13980  geomulcvg  14009  rpnnen2lem1  14344  ruclem4  14363  ruclem8  14366  ruclem11  14369  0bits  14492  gcdval  14549  lcmval  14634  lcmvalOLD  14635  lcmfpr  14679  lcmfunsnlem2  14692  prmreclem2  14940  prmreclem5  14943  vdwapun  15003  mgmnsgrpex  16743  odval  17258  odvalOLD  17261  odf  17264  odfOLD  17280  gexval  17305  gexvalOLD  17307  telgsumfz0  17700  telgsum  17702  srgbinom  17856  abvtrivd  18146  snifpsrbag  18667  psrbaglesupp  18669  psrbagaddcl  18671  psrbaglefi  18673  mplcoe5  18769  mplbas2  18771  ltbwe  18773  psrbag0  18794  psrbagev1  18810  cply1coe0bi  18971  m2cpminvid2lem  19855  pmatcollpw3fi1lem1  19887  pmatcollpw3fi1lem2  19888  pmatcollpw3fi1  19889  idpm2idmp  19902  prdsdsf  21460  prdsxmetlem  21461  prdsmet  21463  imasdsf1olem  21466  prdsbl  21584  xrge0gsumle  21929  xrge0tsms  21930  xrhmeo  22052  pcopt  22131  pcopt2  22132  pcoass  22133  rrxcph  22429  ovoliunnul  22538  ovolicc1  22547  vitalilem5  22649  mbfpos  22686  0pval  22708  0pledm  22710  i1f1lem  22726  i1f1  22727  itg11  22728  itg1addlem3  22735  itg1addlem4  22736  i1fres  22742  itg1climres  22751  mbfi1fseqlem4  22755  mbfi1fseqlem6  22757  mbfi1flimlem  22759  mbfi1flim  22760  xrge0f  22768  itg2ge0  22772  itg2uba  22780  itg2splitlem  22785  itg2monolem1  22787  itg2gt0  22797  itg2cnlem1  22798  ibl0  22823  iblcnlem1  22824  i1fibl  22844  itgeqa  22850  itgcn  22879  dvcmul  22977  dvcmulf  22978  dvexp3  23009  rolle  23021  dveq0  23031  dv11cn  23032  tdeglem4  23088  elply2  23229  elplyd  23235  ply1term  23237  ply0  23241  plyeq0  23244  plypf1  23245  plymullem  23249  dgrlt  23299  plymul0or  23313  dvply1  23316  plydivlem4  23328  elqaalem2  23352  elqaalem2OLD  23355  iaa  23360  aareccl  23361  aannenlem2  23364  tayl0  23396  taylpfval  23399  dvtaylp  23404  pserdvlem2  23462  abelthlem9  23474  logtayl  23684  cxplogb  23802  leibpilem2  23946  leibpi  23947  jensenlem2  23992  jensen  23993  amgmlem  23994  amgm  23995  igamval  24051  vmaval  24119  vmaf  24125  muval  24138  dchrelbas2  24244  dchrinvcl  24260  dchrptlem2  24272  lgseisenlem4  24359  pntrlog2bndlem4  24497  pntrlog2bndlem5  24498  padicval  24534  padicabv  24547  ostth1  24550  axlowdimlem8  25058  axlowdimlem9  25059  axlowdimlem10  25060  axlowdimlem11  25061  axlowdimlem12  25062  axlowdimlem13  25063  axlowdimlem17  25067  2trllemA  25359  2trllemH  25361  2trllemE  25362  2wlklemA  25363  wlkntrllem1  25368  wlkntrllem2  25369  wlkntrllem3  25370  2wlklem  25373  0spth  25380  constr1trl  25397  1pthon  25400  2pthlem2  25405  2wlklem1  25406  2pthon  25411  2pthon3v  25413  usgra2adedgwlkonALT  25423  usgra2wlkspthlem1  25426  usgra2wlkspthlem2  25427  constr3lem2  25453  constr3lem4  25454  constr3lem5  25455  constr3trllem1  25457  constr3trllem2  25458  clwwlkn2  25582  usg2wlkonot  25690  usg2wotspth  25691  0egra0rgra  25743  rusgranumwlkl1  25754  eupath  25788  occllem  27037  0cnfn  27714  0lnfn  27719  nmfn0  27721  nmcexi  27760  nlelchi  27795  xrge0infssOLD  28416  sgnsval  28565  sgnsf  28566  xrge0tsmsd  28622  xrge0iif1  28818  xrge0mulc1cn  28821  gsumesum  28954  esumpfinval  28970  esumpfinvalf  28971  ddeval1  29130  ddeval0  29131  ddemeas  29132  eulerpartlemt  29277  coinfliprv  29388  sgncl  29482  plymul02  29507  plymulx  29509  signsw0glem  29514  signsw0g  29517  signswmnd  29518  signswrid  29519  signstfvn  29530  cvmliftlem4  30083  cvmliftlem5  30084  poimirlem1  32005  poimirlem2  32006  poimirlem3  32007  poimirlem4  32008  poimirlem5  32009  poimirlem6  32010  poimirlem7  32011  poimirlem11  32015  poimirlem12  32016  poimirlem16  32020  poimirlem17  32021  poimirlem19  32023  poimirlem20  32024  poimirlem22  32026  poimirlem23  32027  poimirlem24  32028  poimirlem25  32029  poimirlem28  32032  poimirlem29  32033  poimirlem31  32035  poimirlem32  32036  poimir  32037  broucube  32038  mblfinlem2  32042  mblfinlem3  32043  ismblfin  32045  itg2addnclem  32057  itg2addnclem3  32059  itg2addnc  32060  ftc1anclem3  32083  ftc1anclem5  32085  ftc1anclem7  32087  ftc1anclem8  32088  ftc1anc  32089  dvacos  32093  prdsbnd  32189  heiborlem10  32216  renegclALT  32599  diophrw  35672  monotoddzzfi  35861  zindbi  35865  mncn0  36069  aaitgo  36099  flcidc  36111  dfrcl4  36339  fvrcllb0d  36356  fvrcllb0da  36357  iunrelexp0  36365  corclrcl  36370  relexp0idm  36378  dfrtrcl4  36401  corcltrcl  36402  cotrclrcl  36405  ofsubid  36743  lhe4.4ex1a  36748  dvsconst  36749  dvconstbi  36753  binomcxplemnn0  36768  binomcxplemdvbinom  36772  binomcxplemnotnn0  36775  n0p  37437  climrec  37778  dvnmptdivc  37910  dvnmul  37915  stoweidlem55  38028  fourierdlem62  38144  fourierdlem104  38186  fouriersw  38207  rrxbasefi  38264  ovnval2  38485  hoidmvval  38517  hoidmvlelem1  38535  el1fzopredsuc  38867  fun2dmnopgexmpl  39174  uspgr1ewop  39487  usgr2v1e2w  39491  umgr2v2eedg  39747  umgr2v2e  39748  umgr2v2evd2  39750  2Wlklem  39862  usgr2wlkneq  39948  0spth-av  40015  11wlkdlem4  40028  1wlk2v2elem1  40043  21wlkdlem4  40050  21wlkdlem5  40051  2pthdlem1  40052  21wlkdlem10  40057  31wlkdlem4  40076  31wlkdlem5  40077  3pthdlem1  40078  31wlkdlem10  40083  upgr3v3e3cycl  40094  upgr4cycl4dv4e  40099  eulerpathpr  40152  konigsberglem4  40169  konigsberglem5  40170  usgra2adedglem1  40178  zlmodzxzel  40644  zlmodzxz0  40645  zlmodzxzscm  40646  zlmodzxzadd  40647  zlmodzxznm  40798  zlmodzxzldeplem  40799  zlmodzxzldeplem2  40802  blen0  40891  nn0sumshdiglemB  40939  ex-gt  40956  ex-gte  40957  aacllem  41046
  Copyright terms: Public domain W3C validator