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 ) |
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 ) |