Theorem cbvsumv 14274

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 2751	. 2 ⊢ Ⅎ𝑘𝐴
3		nfcv 2751	. 2 ⊢ Ⅎ𝑗𝐴
4		nfcv 2751	. 2 ⊢ Ⅎ𝑘𝐵
5		nfcv 2751	. 2 ⊢ Ⅎ𝑗𝐶
6	1, 2, 3, 4, 5	cbvsum 14273	1 ⊢ Σ𝑗 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1475  Σcsu 14264

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-xp 5044  df-cnv 5046  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-iota 5768  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-seq 12664  df-sum 14265

This theorem is referenced by:  isumge0  14339  telfsumo  14375  fsumparts  14379  binomlem  14400  incexclem  14407  mertenslem1  14455  mertens  14457  binomfallfaclem2  14610  bpolyval  14619  efaddlem  14662  pwp1fsum  14952  bitsinv2  15003  prmreclem6  15463  ovolicc2lem4  23095  uniioombllem6  23162  plymullem1  23774  plyadd  23777  plymul  23778  coeeu  23785  coeid  23798  dvply1  23843  vieta1  23871  aaliou3  23910  abelthlem8  23997  abelthlem9  23998  abelth  23999  logtayl  24206  ftalem2  24600  ftalem6  24604  dchrsum2  24793  sumdchr2  24795  dchrisumlem1  24978  dchrisum  24981  dchrisum0fval  24994  dchrisum0ff  24996  rpvmasum  25015  mulog2sumlem1  25023  2vmadivsumlem  25029  logsqvma  25031  logsqvma2  25032  selberg  25037  chpdifbndlem1  25042  selberg3lem1  25046  selberg4lem1  25049  pntsval  25061  pntsval2  25065  pntpbnd1  25075  pntlemo  25096  axsegconlem9  25605  hashunif  28949  eulerpartlems  29749  eulerpartlemgs2  29769  fwddifnp1  31442  binomcxplemnotnn0  37577  mccl  38665  sumnnodd  38697  dvnprodlem1  38836  dvnprodlem3  38838  dvnprod  38839  fourierdlem73  39072  fourierdlem112  39111  fourierdlem113  39112  etransclem11  39138  etransclem32  39159  etransclem35  39162  etransc  39176  fsumlesge0  39270  meaiuninclem  39373  omeiunltfirp  39409  hoidmvlelem3  39487  pwdif  40039  altgsumbcALT  41924  nn0sumshdiglemA  42211  nn0sumshdiglemB  42212