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 )