Metamath Proof Explorer
Description: Change bound variable in a product. (Contributed by Scott Fenton, 4Dec2017)


Ref 
Expression 

Hypothesis 
cbvprod.1 
⊢ ( 𝑗 = 𝑘 → 𝐵 = 𝐶 ) 

Assertion 
cbvprodv 
⊢ ∏ 𝑗 ∈ 𝐴 𝐵 = ∏ 𝑘 ∈ 𝐴 𝐶 
Proof
Step 
Hyp 
Ref 
Expression 
1 

cbvprod.1 
⊢ ( 𝑗 = 𝑘 → 𝐵 = 𝐶 ) 
2 

nfcv 
⊢ Ⅎ 𝑘 𝐴 
3 

nfcv 
⊢ Ⅎ 𝑗 𝐴 
4 

nfcv 
⊢ Ⅎ 𝑘 𝐵 
5 

nfcv 
⊢ Ⅎ 𝑗 𝐶 
6 
1 2 3 4 5

cbvprod 
⊢ ∏ 𝑗 ∈ 𝐴 𝐵 = ∏ 𝑘 ∈ 𝐴 𝐶 