Theorem cbvsumvw2

Description: Change bound variable and the set of integers in a sum, using implicit substitution. (Contributed by GG, 1-Sep-2025)

	Ref	Expression
Hypotheses	cbvsumvw2.1	$$⊢A=B$$
	cbvsumvw2.2	$$⊢j=k\to C=D$$
Assertion	cbvsumvw2	$$⊢\sum _{j\in A}C=\sum _{k\in B}D$$

Proof

Step	Hyp	Ref	Expression
1		cbvsumvw2.1	$$⊢A=B$$
2		cbvsumvw2.2	$$⊢j=k\to C=D$$
3	2	cbvsumv	$$⊢\sum _{j\in A}C=\sum _{k\in A}D$$
4	1	sumeq1i	$$⊢\sum _{k\in A}D=\sum _{k\in B}D$$
5	3 4	eqtri	$$⊢\sum _{j\in A}C=\sum _{k\in B}D$$