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		fveq2	⊢ ( 𝑥 = 𝑦 → ( 𝑧 ‘ 𝑥 ) = ( 𝑧 ‘ 𝑦 ) )
3	2 1	eleq12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 ↔ ( 𝑧 ‘ 𝑦 ) ∈ 𝐶 ) )
4	3	cbvralvw	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑧 ‘ 𝑦 ) ∈ 𝐶 )
5	4	anbi2i	⊢ ( ( 𝑧 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 ) ↔ ( 𝑧 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑧 ‘ 𝑦 ) ∈ 𝐶 ) )
6	5	abbii	⊢ { 𝑧 ∣ ( 𝑧 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 ) } = { 𝑧 ∣ ( 𝑧 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑧 ‘ 𝑦 ) ∈ 𝐶 ) }
7		dfixp	⊢ X 𝑥 ∈ 𝐴 𝐵 = { 𝑧 ∣ ( 𝑧 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 ) }
8		dfixp	⊢ X 𝑦 ∈ 𝐴 𝐶 = { 𝑧 ∣ ( 𝑧 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑧 ‘ 𝑦 ) ∈ 𝐶 ) }
9	6 7 8	3eqtr4i	⊢ X 𝑥 ∈ 𝐴 𝐵 = X 𝑦 ∈ 𝐴 𝐶