Metamath Proof Explorer

Theorem esumeq1

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

Ref Expression
Assertion esumeq1 
|- ( A = B -> sum* k e. A C = sum* k e. B C )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( A = B -> A = B )
2 eqidd 
 |-  ( A = B -> C = C )
3 1 2 esumeq12d 
 |-  ( A = B -> sum* k e. A C = sum* k e. B C )