This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cbvprodi

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

Ref Expression
Hypotheses cbvprodi.1 ⊢ Ⅎ 𝑘 𝐵
cbvprodi.2 ⊢ Ⅎ 𝑗 𝐶
cbvprodi.3 ⊢ ( 𝑗 = 𝑘 → 𝐵 = 𝐶 )
Assertion cbvprodi ∏ 𝑗 ∈ 𝐴 𝐵 = ∏ 𝑘 ∈ 𝐴 𝐶

Proof

Step Hyp Ref Expression
1 cbvprodi.1 ⊢ Ⅎ 𝑘 𝐵
2 cbvprodi.2 ⊢ Ⅎ 𝑗 𝐶
3 cbvprodi.3 ⊢ ( 𝑗 = 𝑘 → 𝐵 = 𝐶 )
4 nfcv ⊢ Ⅎ 𝑘 𝐴
5 nfcv ⊢ Ⅎ 𝑗 𝐴
6 3 4 5 1 2 cbvprod ⊢ ∏ 𝑗 ∈ 𝐴 𝐵 = ∏ 𝑘 ∈ 𝐴 𝐶