Metamath Proof Explorer

Theorem prodeq2

Description: Equality theorem for product. (Contributed by Scott Fenton, 4-Dec-2017)

Ref Expression
Assertion prodeq2 
|- ( A. k e. A B = C -> prod_ k e. A B = prod_ 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 prodeq2ii 
 |-  ( A. k e. A ( _I ` B ) = ( _I ` C ) -> prod_ k e. A B = prod_ k e. A C )
4 2 3 syl 
 |-  ( A. k e. A B = C -> prod_ k e. A B = prod_ k e. A C )