Theorem esumeq1d

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

	Ref	Expression
Hypotheses	esumeq1d.0	|- F/ k ph
	esumeq1d.1	|- ( ph -> A = B )
Assertion	esumeq1d	|- ( ph -> sum* k e. A C = sum* k e. B C )

Proof

Step	Hyp	Ref	Expression
1		esumeq1d.0	|- F/ k ph
2		esumeq1d.1	|- ( ph -> A = B )
3		eqidd	|- ( ( ph /\ k e. A ) -> C = C )
4	1 2 3	esumeq12dvaf	|- ( ph -> sum* k e. A C = sum* k e. B C )