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 𝑥𝐵 𝐶 )