Theorem cbvixpv

Description: Change bound variable in an indexed Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Hypothesis	cbvixpv.1	⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐶 )
Assertion	cbvixpv	⊢ X 𝑥 ∈ 𝐴 𝐵 = X 𝑦 ∈ 𝐴 𝐶

Proof

Step	Hyp	Ref	Expression
1		cbvixpv.1	⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐶 )
2		nfcv	⊢ Ⅎ 𝑦 𝐵
3		nfcv	⊢ Ⅎ 𝑥 𝐶
4	2 3 1	cbvixp	⊢ X 𝑥 ∈ 𝐴 𝐵 = X 𝑦 ∈ 𝐴 𝐶