Theorem esumeq1

Description: Equality theorem for an extended sum. (Contributed by Thierry Arnoux, 18-Feb-2017)

	Ref	Expression
Assertion	esumeq1	$$⊢A=B\to \underset{k\in A}{{\sum }^{*}}C=\underset{k\in B}{{\sum }^{*}}C$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢A=B\to A=B$$
2		eqidd	$$⊢A=B\to C=C$$
3	1 2	esumeq12d	$$⊢A=B\to \underset{k\in A}{{\sum }^{*}}C=\underset{k\in B}{{\sum }^{*}}C$$