Metamath Proof Explorer


Theorem esumeq12dva

Description: Equality deduction for extended sum. (Contributed by Thierry Arnoux, 18-Feb-2017) (Revised by Thierry Arnoux, 29-Jun-2017)

Ref Expression
Hypotheses esumeq12dva.1
|- ( ph -> A = B )
esumeq12dva.2
|- ( ( ph /\ k e. A ) -> C = D )
Assertion esumeq12dva
|- ( ph -> sum* k e. A C = sum* k e. B D )

Proof

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