Theorem cbvsumv 15641

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:   𝑗,𝑘,𝐴   𝐵,𝑘   𝐶,𝑗

Allowed substitution hints:   𝐵(𝑗)   𝐶(𝑘)

Proof of Theorem cbvsumv

Step	Hyp	Ref	Expression
1		cbvsum.1	. 2 ⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶)
2		nfcv 2903	. 2 ⊢ Ⅎ𝑘𝐴
3		nfcv 2903	. 2 ⊢ Ⅎ𝑗𝐴
4		nfcv 2903	. 2 ⊢ Ⅎ𝑘𝐵
5		nfcv 2903	. 2 ⊢ Ⅎ𝑗𝐶
6	1, 2, 3, 4, 5	cbvsum 15640	1 ⊢ Σ𝑗 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1541  Σcsu 15631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-11 2154  ax-12 2171  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-xp 5682  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-iota 6495  df-fv 6551  df-ov 7411  df-oprab 7412  df-mpo 7413  df-frecs 8265  df-wrecs 8296  df-recs 8370  df-rdg 8409  df-seq 13966  df-sum 15632

This theorem is referenced by:  isumge0  15711  telfsumo  15747  fsumparts  15751  binomlem  15774  incexclem  15781  pwdif  15813  mertenslem1  15829  mertens  15831  binomfallfaclem2  15983  bpolyval  15992  efaddlem  16035  pwp1fsum  16333  bitsinv2  16383  prmreclem6  16853  ovolicc2lem4  25036  uniioombllem6  25104  plymullem1  25727  plyadd  25730  plymul  25731  coeeu  25738  coeid  25751  dvply1  25796  vieta1  25824  aaliou3  25863  abelthlem8  25950  abelthlem9  25951  abelth  25952  logtayl  26167  ftalem2  26575  ftalem6  26579  dchrsum2  26768  sumdchr2  26770  dchrisumlem1  26989  dchrisum  26992  dchrisum0fval  27005  dchrisum0ff  27007  rpvmasum  27026  mulog2sumlem1  27034  2vmadivsumlem  27040  logsqvma  27042  logsqvma2  27043  selberg  27048  chpdifbndlem1  27053  selberg3lem1  27057  selberg4lem1  27060  pntsval  27072  pntsval2  27076  pntpbnd1  27086  pntlemo  27107  axsegconlem9  28180  hashunif  32013  eulerpartlems  33354  eulerpartlemgs2  33374  breprexplema  33637  breprexplemc  33639  breprexp  33640  hgt750lema  33664  fwddifnp1  35132  sticksstones16  40973  sticksstones17  40974  sticksstones18  40975  sticksstones21  40978  binomcxplemnotnn0  43105  mccl  44304  sumnnodd  44336  dvnprodlem1  44652  dvnprodlem3  44654  dvnprod  44655  fourierdlem73  44885  fourierdlem112  44924  fourierdlem113  44925  etransclem11  44951  etransclem32  44972  etransclem35  44975  etransc  44989  fsumlesge0  45083  meaiuninclem  45186  omeiunltfirp  45225  hoidmvlelem3  45303  altgsumbcALT  47019  nn0sumshdiglemA  47295  nn0sumshdiglemB  47296