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

Theorem c0ex 9611
Description: 0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
Assertion
Ref Expression
c0ex

Proof of Theorem c0ex
StepHypRef Expression
1 0cn 9609 . 2
21elexi 3119 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1818   cvv 3109   cc 9511  0cc0 9513
This theorem is referenced by:  ofsubeq0  10558  ofsubge0  10560  elnn0  10822  un0mulcl  10855  frnnn0supp  10874  frnnn0fsupp  10876  nn0ssz  10910  nn0ind-raph  10989  xaddval  11451  xmulval  11453  ser0f  12160  facnn  12355  fac0  12356  bcval  12382  prhash2ex  12464  snopiswrd  12556  wrdexb  12558  s1rn  12611  repsw1  12755  cshw1  12790  s1co  12799  wrdlen2i  12884  wrd2pr2op  12885  wwlktovf1  12895  sgnval  12921  iserge0  13483  sum0  13543  sumz  13544  fsumss  13547  fsumser  13552  isumless  13657  geomulcvg  13685  rpnnen2lem1  13948  ruclem4  13967  ruclem8  13970  ruclem11  13973  0bits  14089  gcdval  14146  prmreclem2  14435  prmreclem5  14438  vdwapun  14492  mgmnsgrpex  16049  odval  16558  odf  16561  gexval  16598  telgsumfz0  17021  telgsum  17023  srgbinom  17196  abvtrivd  17489  snifpsrbag  18015  psrbaglesupp  18017  psrbagaddcl  18020  psrbaglefi  18023  mplcoe5  18131  mplbas2  18134  ltbwe  18137  psrbag0  18159  psrbagev1  18177  cply1coe0bi  18342  m2cpminvid2lem  19255  pmatcollpw3fi1lem1  19287  pmatcollpw3fi1lem2  19288  pmatcollpw3fi1  19289  idpm2idmp  19302  prdsdsf  20870  prdsxmetlem  20871  prdsmet  20873  imasdsf1olem  20876  prdsbl  20994  xrge0gsumle  21338  xrge0tsms  21339  xrhmeo  21446  pcopt  21522  pcopt2  21523  pcoass  21524  rrxcph  21824  ovoliunnul  21918  ovolicc1  21927  vitalilem5  22021  mbfpos  22058  0pval  22078  0pledm  22080  i1f1lem  22096  i1f1  22097  itg11  22098  itg1addlem3  22105  itg1addlem4  22106  i1fres  22112  itg1climres  22121  mbfi1fseqlem4  22125  mbfi1fseqlem6  22127  mbfi1flimlem  22129  mbfi1flim  22130  xrge0f  22138  itg2ge0  22142  itg2uba  22150  itg2splitlem  22155  itg2monolem1  22157  itg2gt0  22167  itg2cnlem1  22168  ibl0  22193  iblcnlem1  22194  i1fibl  22214  itgeqa  22220  itgcn  22249  dvcmul  22347  dvcmulf  22348  dvexp3  22379  rolle  22391  dveq0  22401  dv11cn  22402  tdeglem4  22458  elply2  22593  elplyd  22599  ply1term  22601  ply0  22605  plyeq0  22608  plypf1  22609  plymullem  22613  dgrlt  22663  plymul0or  22677  dvply1  22680  plydivlem4  22692  elqaalem2  22716  iaa  22721  aareccl  22722  aannenlem2  22725  tayl0  22757  taylpfval  22760  dvtaylp  22765  pserdvlem2  22823  abelthlem9  22835  logtayl  23041  leibpilem2  23272  leibpi  23273  jensenlem2  23317  jensen  23318  amgmlem  23319  amgm  23320  vmaval  23387  vmaf  23393  muval  23406  dchrelbas2  23512  dchrinvcl  23528  dchrptlem2  23540  lgseisenlem4  23627  pntrlog2bndlem4  23765  pntrlog2bndlem5  23766  padicval  23802  padicabv  23815  ostth1  23818  axlowdimlem8  24252  axlowdimlem9  24253  axlowdimlem10  24254  axlowdimlem11  24255  axlowdimlem12  24256  axlowdimlem13  24257  axlowdimlem17  24261  2trllemA  24552  2trllemH  24554  2trllemE  24555  2wlklemA  24556  wlkntrllem1  24561  wlkntrllem2  24562  wlkntrllem3  24563  2wlklem  24566  0spth  24573  constr1trl  24590  1pthon  24593  2pthlem2  24598  2wlklem1  24599  2pthon  24604  2pthon3v  24606  usgra2adedgwlkonALT  24616  usgra2wlkspthlem1  24619  usgra2wlkspthlem2  24620  constr3lem2  24646  constr3lem4  24647  constr3lem5  24648  constr3trllem1  24650  constr3trllem2  24651  clwwlkn2  24775  usg2wlkonot  24883  usg2wotspth  24884  0egra0rgra  24936  rusgranumwlkl1  24947  eupath  24981  occllem  26221  0cnfn  26899  0lnfn  26904  nmfn0  26906  nmcexi  26945  nlelchi  26980  xrge0infss  27580  sgnsval  27718  sgnsf  27719  xrge0tsmsd  27775  xrge0iif1  27920  xrge0mulc1cn  27923  gsumesum  28067  esumpfinval  28081  esumpfinvalf  28082  ddeval1  28206  ddeval0  28207  ddemeas  28208  eulerpartlemt  28310  coinfliprv  28421  sgncl  28477  plymul02  28503  plymulx  28505  signsw0glem  28510  signsw0g  28513  signswmnd  28514  signswrid  28515  signstfvn  28526  igamval  28589  cvmliftlem4  28733  cvmliftlem5  28734  relexp0  29052  mblfinlem2  30052  mblfinlem3  30053  ismblfin  30055  itg2addnclem  30066  itg2addnclem3  30068  itg2addnc  30069  ftc1anclem3  30092  ftc1anclem5  30094  ftc1anclem7  30096  ftc1anclem8  30097  ftc1anc  30098  dvacos  30104  prdsbnd  30289  heiborlem10  30316  diophrw  30692  monotoddzzfi  30878  zindbi  30882  mncn0  31088  aaitgo  31111  flcidc  31123  lcmval  31198  ofsubid  31229  lhe4.4ex1a  31234  dvsconst  31235  dvconstbi  31239  binomcxplemnn0  31254  binomcxplemdvbinom  31258  binomcxplemnotnn0  31261  n0p  31437  climrec  31609  dvnmptdivc  31735  dvnmul  31740  stoweidlem55  31837  fourierdlem62  31951  fourierdlem104  31993  fouriersw  32014  usgra2adedglem1  32356  zlmodzxzel  32944  zlmodzxz0  32945  zlmodzxzscm  32946  zlmodzxzadd  32947  zlmodzxznm  33098  zlmodzxzldeplem  33099  zlmodzxzldeplem2  33102  ex-gt  33122  ex-gte  33123  aacllem  33216  renegclALT  34694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854  ax-ext 2435  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-mulcl 9575  ax-i2m1 9581
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-v 3111
  Copyright terms: Public domain W3C validator