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

Theorem sumex 13510
 Description: A sum is a set. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
Assertion
Ref Expression
sumex

Proof of Theorem sumex
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-sum 13509 . 2
2 iotaex 5573 . 2
31, 2eqeltri 2541 1
 Colors of variables: wff setvar class Syntax hints:  \/wo 368  /\wa 369  =wceq 1395  E.wex 1612  e.wcel 1818  E.wrex 2808   cvv 3109  [_csb 3434  C_wss 3475  ifcif 3941   class class class wbr 4452  e.cmpt 4510  iotacio 5554  -1-1-onto->wf1o 5592  cfv 5593  (class class class)co 6296  0cc0 9513  1c1 9514   caddc 9516   cn 10561   cz 10889   cuz 11110   cfz 11701  seqcseq 12107   cli 13307  sum_`csu 13508 This theorem is referenced by:  fsumrlim  13625  fsumo1  13626  efval  13815  efcvgfsum  13821  eftlub  13844  bitsinv2  14093  bitsinv  14098  lebnumlem3  21463  isi1f  22081  itg1val  22090  itg1climres  22121  itgex  22177  itgfsum  22233  dvmptfsum  22376  plyeq0lem  22607  plyaddlem1  22610  plymullem1  22611  coeeulem  22621  coeid2  22636  plyco  22638  coemullem  22647  coemul  22649  aareccl  22722  aaliou3lem5  22743  aaliou3lem6  22744  aaliou3lem7  22745  taylpval  22762  psercn  22821  pserdvlem2  22823  pserdv  22824  abelthlem6  22831  abelthlem8  22834  abelthlem9  22835  logtayl  23041  leibpi  23273  basellem3  23356  chtval  23384  chpval  23396  sgmval  23416  muinv  23469  dchrvmasumlem1  23680  dchrisum0fval  23690  dchrisum0fno1  23696  dchrisum0lem3  23704  dchrisum0  23705  mulogsum  23717  logsqvma2  23728  selberglem1  23730  pntsval  23757  ecgrtg  24286  esumpcvgval  28084  esumcvg  28092  eulerpartlemsv1  28295  signsplypnf  28507  signsvvfval  28535  binomcxplemnotnn0  31261  stoweidlem11  31793  stoweidlem26  31808  fourierdlem112  32001  aacllem  33216 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-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-nul 4581 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-v 3111  df-sbc 3328  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-sn 4030  df-pr 4032  df-uni 4250  df-iota 5556  df-sum 13509
 Copyright terms: Public domain W3C validator