Metamath Proof Explorer

Theorem ixpeq1

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

Ref Expression
Assertion ixpeq1 ⊢ A = B → ⨉ x ∈ A C = ⨉ x ∈ B C

Proof

Step Hyp Ref Expression
1 fneq2 ⊢ A = B → f Fn A ↔ f Fn B
2 raleq ⊢ A = B → ∀ x ∈ A f ⁡ x ∈ C ↔ ∀ x ∈ B f ⁡ x ∈ C
3 1 2 anbi12d ⊢ A = B → f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ C ↔ f Fn B ∧ ∀ x ∈ B f ⁡ x ∈ C
4 3 abbidv ⊢ A = B → f | f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ C = f | f Fn B ∧ ∀ x ∈ B f ⁡ x ∈ C
5 dfixp ⊢ ⨉ x ∈ A C = f | f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ C
6 dfixp ⊢ ⨉ x ∈ B C = f | f Fn B ∧ ∀ x ∈ B f ⁡ x ∈ C
7 4 5 6 3eqtr4g ⊢ A = B → ⨉ x ∈ A C = ⨉ x ∈ B C