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

Metamath Proof Explorer

Theorem ixpeq1

Description: Equality theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006)

Ref Expression
Assertion ixpeq1 ( 𝐴 = 𝐵 → X 𝑥 ∈ 𝐴 𝐶 = X 𝑥 ∈ 𝐵 𝐶 )

Proof

Step Hyp Ref Expression
1 fneq2 ⊢ ( 𝐴 = 𝐵 → ( 𝑓 Fn 𝐴 ↔ 𝑓 Fn 𝐵 ) )
2 raleq ⊢ ( 𝐴 = 𝐵 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) )
3 1 2 anbi12d ⊢ ( 𝐴 = 𝐵 → ( ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ↔ ( 𝑓 Fn 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) )
4 3 abbidv ⊢ ( 𝐴 = 𝐵 → { 𝑓 ∣ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) } = { 𝑓 ∣ ( 𝑓 Fn 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) } )
5 dfixp ⊢ X 𝑥 ∈ 𝐴 𝐶 = { 𝑓 ∣ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) }
6 dfixp ⊢ X 𝑥 ∈ 𝐵 𝐶 = { 𝑓 ∣ ( 𝑓 Fn 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) }
7 4 5 6 3eqtr4g ⊢ ( 𝐴 = 𝐵 → X 𝑥 ∈ 𝐴 𝐶 = X 𝑥 ∈ 𝐵 𝐶 )