Metamath Proof Explorer

Theorem sumeq2

Description: Equality theorem for sum. (Contributed by NM, 11-Dec-2005) (Revised by Mario Carneiro, 13-Jul-2013)

Ref Expression
Assertion sumeq2 
|- ( A. k e. A B = C -> sum_ k e. A B = sum_ k e. A C )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( B = C -> ( _I ` B ) = ( _I ` C ) )
2 1 ralimi 
 |-  ( A. k e. A B = C -> A. k e. A ( _I ` B ) = ( _I ` C ) )
3 sumeq2ii 
 |-  ( A. k e. A ( _I ` B ) = ( _I ` C ) -> sum_ k e. A B = sum_ k e. A C )
4 2 3 syl 
 |-  ( A. k e. A B = C -> sum_ k e. A B = sum_ k e. A C )