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

Metamath Proof Explorer

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 𝑦 ∈ 𝐴 𝐶