Metamath Proof Explorer

Theorem cbvprodv

Description: Change bound variable in a product. (Contributed by Scott Fenton, 4-Dec-2017)

Ref Expression
Hypothesis cbvprod.1 
|- ( j = k -> B = C )
Assertion cbvprodv 
|- prod_ j e. A B = prod_ k e. A C

Proof

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