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.

Step	Hyp	Ref	Expression
1		df-sum 13509	. 2
2		iotaex 5573	. 2
3	1, 2	eqeltri 2541	1

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