Theorem cbvsumv 13518

Description: Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jul-2013.)

Hypothesis

Ref	Expression
cbvsum.1

Assertion

Ref	Expression
cbvsumv

Distinct variable groups:   ,,   ,   ,

Proof of Theorem cbvsumv

Step	Hyp	Ref	Expression
1		cbvsum.1	. 2
2		nfcv 2619	. 2
3		nfcv 2619	. 2
4		nfcv 2619	. 2
5		nfcv 2619	. 2
6	1, 2, 3, 4, 5	cbvsum 13517	1

Syntax hints:  ->wi 4  =wceq 1395  sum_csu 13508

This theorem is referenced by:  isumge0  13581  telfsumo  13616  fsumparts  13620  binomlem  13641  incexclem  13648  mertenslem1  13693  mertens  13695  efaddlem  13828  bitsinv2  14093  prmreclem6  14439  ovolicc2lem4  21931  uniioombllem6  21997  plymullem1  22611  plyadd  22614  plymul  22615  coeeu  22622  coeid  22635  dvply1  22680  vieta1  22708  aaliou3  22747  abelthlem8  22834  abelthlem9  22835  abelth  22836  logtayl  23041  ftalem2  23347  ftalem6  23351  dchrsum2  23543  sumdchr2  23545  dchrisumlem1  23674  dchrisum  23677  dchrisum0fval  23690  dchrisum0ff  23692  rpvmasum  23711  mulog2sumlem1  23719  2vmadivsumlem  23725  logsqvma  23727  logsqvma2  23728  selberg  23733  chpdifbndlem1  23738  selberg3lem1  23742  selberg4lem1  23745  pntsval  23757  pntsval2  23761  pntpbnd1  23771  pntlemo  23792  axsegconlem9  24228  hashunif  27605  eulerpartlems  28299  eulerpartlemgs2  28319  binomfallfaclem2  29162  bpolyval  29811  binomcxplemnotnn0  31261  mccl  31606  sumnnodd  31636  dvnprodlem1  31743  dvnprodlem3  31745  dvnprod  31746  fourierdlem73  31962  fourierdlem112  32001  fourierdlem113  32002  etransclem11  32028  etransclem32  32049  etransclem35  32052  etransc  32066  altgsumbcALT  32942

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

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-mpt 4512  df-cnv 5012  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fv 5601  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-recs 7061  df-rdg 7095  df-seq 12108  df-sum 13509