Metamath Proof Explorer


Theorem esumeq2sdv

Description: Equality deduction for extended sum. (Contributed by Thierry Arnoux, 25-Dec-2016)

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

Proof

Step Hyp Ref Expression
1 esumeq2sdv.1
 |-  ( ph -> B = C )
2 1 adantr
 |-  ( ( ph /\ k e. A ) -> B = C )
3 2 esumeq2dv
 |-  ( ph -> sum* k e. A B = sum* k e. A C )