Theorem cbvixp

Description: Change bound variable in an indexed Cartesian product. (Contributed by Jeff Madsen, 20-Jun-2011)

	Ref	Expression
Hypotheses	cbvixp.1	⊢ Ⅎ 𝑦 𝐵
	cbvixp.2	⊢ Ⅎ 𝑥 𝐶
	cbvixp.3	⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐶 )
Assertion	cbvixp	⊢ X 𝑥 ∈ 𝐴 𝐵 = X 𝑦 ∈ 𝐴 𝐶

Proof

Step	Hyp	Ref	Expression
1		cbvixp.1	⊢ Ⅎ 𝑦 𝐵
2		cbvixp.2	⊢ Ⅎ 𝑥 𝐶
3		cbvixp.3	⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐶 )
4	1	nfel2	⊢ Ⅎ 𝑦 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵
5	2	nfel2	⊢ Ⅎ 𝑥 ( 𝑓 ‘ 𝑦 ) ∈ 𝐶
6		fveq2	⊢ ( 𝑥 = 𝑦 → ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑦 ) )
7	6 3	eleq12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ↔ ( 𝑓 ‘ 𝑦 ) ∈ 𝐶 ) )
8	4 5 7	cbvralw	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) ∈ 𝐶 )
9	8	anbi2i	⊢ ( ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) ∈ 𝐶 ) )
10	9	abbii	⊢ { 𝑓 ∣ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) } = { 𝑓 ∣ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) ∈ 𝐶 ) }
11		dfixp	⊢ X 𝑥 ∈ 𝐴 𝐵 = { 𝑓 ∣ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) }
12		dfixp	⊢ X 𝑦 ∈ 𝐴 𝐶 = { 𝑓 ∣ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) ∈ 𝐶 ) }
13	10 11 12	3eqtr4i	⊢ X 𝑥 ∈ 𝐴 𝐵 = X 𝑦 ∈ 𝐴 𝐶