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 ⊢ Ⅎ _ k B
cbvprodi.2 ⊢ Ⅎ _ j C
cbvprodi.3 ⊢ j = k → B = C
Assertion cbvprodi ⊢ ∏ j ∈ A B = ∏ k ∈ A C

Proof

Step Hyp Ref Expression
1 cbvprodi.1 ⊢ Ⅎ _ k B
2 cbvprodi.2 ⊢ Ⅎ _ j C
3 cbvprodi.3 ⊢ j = k → B = C
4 nfcv ⊢ Ⅎ _ k A
5 nfcv ⊢ Ⅎ _ j A
6 3 4 5 1 2 cbvprod ⊢ ∏ j ∈ A B = ∏ k ∈ A C