Theorem esumeq1d

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

	Ref	Expression
Hypotheses	esumeq1d.0	$$⊢Ⅎk\phi$$
	esumeq1d.1	$$⊢\phi \to A=B$$
Assertion	esumeq1d	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}C=\underset{k\in B}{{\sum }^{*}}C$$

Proof

Step	Hyp	Ref	Expression
1		esumeq1d.0	$$⊢Ⅎk\phi$$
2		esumeq1d.1	$$⊢\phi \to A=B$$
3		eqidd	$$⊢\left(\phi \wedge k\in A\right)\to C=C$$
4	1 2 3	esumeq12dvaf	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}C=\underset{k\in B}{{\sum }^{*}}C$$