Theorem cbvsumv 15408

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

Syntax hints:   → wi 4   = wceq 1539  Σcsu 15397

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-xp 5595  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-iota 6391  df-fv 6441  df-ov 7278  df-oprab 7279  df-mpo 7280  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-seq 13722  df-sum 15398

This theorem is referenced by:  isumge0  15478  telfsumo  15514  fsumparts  15518  binomlem  15541  incexclem  15548  pwdif  15580  mertenslem1  15596  mertens  15598  binomfallfaclem2  15750  bpolyval  15759  efaddlem  15802  pwp1fsum  16100  bitsinv2  16150  prmreclem6  16622  ovolicc2lem4  24684  uniioombllem6  24752  plymullem1  25375  plyadd  25378  plymul  25379  coeeu  25386  coeid  25399  dvply1  25444  vieta1  25472  aaliou3  25511  abelthlem8  25598  abelthlem9  25599  abelth  25600  logtayl  25815  ftalem2  26223  ftalem6  26227  dchrsum2  26416  sumdchr2  26418  dchrisumlem1  26637  dchrisum  26640  dchrisum0fval  26653  dchrisum0ff  26655  rpvmasum  26674  mulog2sumlem1  26682  2vmadivsumlem  26688  logsqvma  26690  logsqvma2  26691  selberg  26696  chpdifbndlem1  26701  selberg3lem1  26705  selberg4lem1  26708  pntsval  26720  pntsval2  26724  pntpbnd1  26734  pntlemo  26755  axsegconlem9  27293  hashunif  31126  eulerpartlems  32327  eulerpartlemgs2  32347  breprexplema  32610  breprexplemc  32612  breprexp  32613  hgt750lema  32637  fwddifnp1  34467  sticksstones16  40118  sticksstones17  40119  sticksstones18  40120  sticksstones21  40123  binomcxplemnotnn0  41974  mccl  43139  sumnnodd  43171  dvnprodlem1  43487  dvnprodlem3  43489  dvnprod  43490  fourierdlem73  43720  fourierdlem112  43759  fourierdlem113  43760  etransclem11  43786  etransclem32  43807  etransclem35  43810  etransc  43824  fsumlesge0  43915  meaiuninclem  44018  omeiunltfirp  44057  hoidmvlelem3  44135  altgsumbcALT  45689  nn0sumshdiglemA  45965  nn0sumshdiglemB  45966