Theorem cbvsumv 15146

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

Syntax hints:   → wi 4   = wceq 1542  Σcsu 15135

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-ex 1787  df-nf 1791  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ral 3058  df-rex 3059  df-rab 3062  df-v 3400  df-sbc 3681  df-csb 3791  df-un 3848  df-in 3850  df-ss 3860  df-if 4415  df-sn 4517  df-pr 4519  df-op 4523  df-uni 4797  df-br 5031  df-opab 5093  df-mpt 5111  df-xp 5531  df-cnv 5533  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6129  df-iota 6297  df-fv 6347  df-ov 7173  df-oprab 7174  df-mpo 7175  df-wrecs 7976  df-recs 8037  df-rdg 8075  df-seq 13461  df-sum 15136

This theorem is referenced by:  isumge0  15214  telfsumo  15250  fsumparts  15254  binomlem  15277  incexclem  15284  pwdif  15316  mertenslem1  15332  mertens  15334  binomfallfaclem2  15486  bpolyval  15495  efaddlem  15538  pwp1fsum  15836  bitsinv2  15886  prmreclem6  16357  ovolicc2lem4  24272  uniioombllem6  24340  plymullem1  24963  plyadd  24966  plymul  24967  coeeu  24974  coeid  24987  dvply1  25032  vieta1  25060  aaliou3  25099  abelthlem8  25186  abelthlem9  25187  abelth  25188  logtayl  25403  ftalem2  25811  ftalem6  25815  dchrsum2  26004  sumdchr2  26006  dchrisumlem1  26225  dchrisum  26228  dchrisum0fval  26241  dchrisum0ff  26243  rpvmasum  26262  mulog2sumlem1  26270  2vmadivsumlem  26276  logsqvma  26278  logsqvma2  26279  selberg  26284  chpdifbndlem1  26289  selberg3lem1  26293  selberg4lem1  26296  pntsval  26308  pntsval2  26312  pntpbnd1  26322  pntlemo  26343  axsegconlem9  26871  hashunif  30701  eulerpartlems  31897  eulerpartlemgs2  31917  breprexplema  32180  breprexplemc  32182  breprexp  32183  hgt750lema  32207  fwddifnp1  34105  binomcxplemnotnn0  41512  mccl  42681  sumnnodd  42713  dvnprodlem1  43029  dvnprodlem3  43031  dvnprod  43032  fourierdlem73  43262  fourierdlem112  43301  fourierdlem113  43302  etransclem11  43328  etransclem32  43349  etransclem35  43352  etransc  43366  fsumlesge0  43457  meaiuninclem  43560  omeiunltfirp  43599  hoidmvlelem3  43677  altgsumbcALT  45223  nn0sumshdiglemA  45499  nn0sumshdiglemB  45500