Metamath Proof Explorer

Theorem prodeq1

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

Ref Expression
Assertion prodeq1 
|- ( A = B -> prod_ k e. A C = prod_ k e. B C )

Proof

Step Hyp Ref Expression
1 nfcv 
 |-  F/_ k A
2 nfcv 
 |-  F/_ k B
3 1 2 prodeq1f 
 |-  ( A = B -> prod_ k e. A C = prod_ k e. B C )