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

Metamath Proof Explorer

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