Theorem esumeq2dv

Description: Equality deduction for extended sum. (Contributed by Thierry Arnoux, 2-Jan-2017)

	Ref	Expression
Hypothesis	esumeq2dv.1	|- ( ( ph /\ k e. A ) -> B = C )
Assertion	esumeq2dv	|- ( ph -> sum* k e. A B = sum* k e. A C )

Proof

Step	Hyp	Ref	Expression
1		esumeq2dv.1	|- ( ( ph /\ k e. A ) -> B = C )
2		nfv	|- F/ k ph
3	1	ralrimiva	|- ( ph -> A. k e. A B = C )
4	2 3	esumeq2d	|- ( ph -> sum* k e. A B = sum* k e. A C )