Theorem cbvsumv 15053

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

Syntax hints:   → wi 4   = wceq 1537  Σcsu 15042

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-xp 5561  df-cnv 5563  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-iota 6314  df-fv 6363  df-ov 7159  df-oprab 7160  df-mpo 7161  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-seq 13371  df-sum 15043

This theorem is referenced by:  isumge0  15121  telfsumo  15157  fsumparts  15161  binomlem  15184  incexclem  15191  pwdif  15223  mertenslem1  15240  mertens  15242  binomfallfaclem2  15394  bpolyval  15403  efaddlem  15446  pwp1fsum  15742  bitsinv2  15792  prmreclem6  16257  ovolicc2lem4  24121  uniioombllem6  24189  plymullem1  24804  plyadd  24807  plymul  24808  coeeu  24815  coeid  24828  dvply1  24873  vieta1  24901  aaliou3  24940  abelthlem8  25027  abelthlem9  25028  abelth  25029  logtayl  25243  ftalem2  25651  ftalem6  25655  dchrsum2  25844  sumdchr2  25846  dchrisumlem1  26065  dchrisum  26068  dchrisum0fval  26081  dchrisum0ff  26083  rpvmasum  26102  mulog2sumlem1  26110  2vmadivsumlem  26116  logsqvma  26118  logsqvma2  26119  selberg  26124  chpdifbndlem1  26129  selberg3lem1  26133  selberg4lem1  26136  pntsval  26148  pntsval2  26152  pntpbnd1  26162  pntlemo  26183  axsegconlem9  26711  hashunif  30528  eulerpartlems  31618  eulerpartlemgs2  31638  breprexplema  31901  breprexplemc  31903  breprexp  31904  hgt750lema  31928  fwddifnp1  33626  binomcxplemnotnn0  40737  mccl  41928  sumnnodd  41960  dvnprodlem1  42280  dvnprodlem3  42282  dvnprod  42283  fourierdlem73  42513  fourierdlem112  42552  fourierdlem113  42553  etransclem11  42579  etransclem32  42600  etransclem35  42603  etransc  42617  fsumlesge0  42708  meaiuninclem  42811  omeiunltfirp  42850  hoidmvlelem3  42928  altgsumbcALT  44450  nn0sumshdiglemA  44728  nn0sumshdiglemB  44729