Metamath Proof Explorer

Theorem ixpeq1i

Description: Equality inference for infinite Cartesian product. (Contributed by GG, 1-Sep-2025)

Ref Expression
Hypothesis ixpeq1i.1 ⊢ A = B
Assertion ixpeq1i ⊢ ⨉ x ∈ A C = ⨉ x ∈ B C

Proof

Step Hyp Ref Expression
1 ixpeq1i.1 ⊢ A = B
2 1 eleq2i ⊢ x ∈ A ↔ x ∈ B
3 2 abbii ⊢ x | x ∈ A = x | x ∈ B
4 3 fneq2i ⊢ f Fn x | x ∈ A ↔ f Fn x | x ∈ B
5 2 imbi1i ⊢ x ∈ A → f ⁡ x ∈ C ↔ x ∈ B → f ⁡ x ∈ C
6 5 ralbii2 ⊢ ∀ x ∈ A f ⁡ x ∈ C ↔ ∀ x ∈ B f ⁡ x ∈ C
7 4 6 anbi12i ⊢ f Fn x | x ∈ A ∧ ∀ x ∈ A f ⁡ x ∈ C ↔ f Fn x | x ∈ B ∧ ∀ x ∈ B f ⁡ x ∈ C
8 7 abbii ⊢ f | f Fn x | x ∈ A ∧ ∀ x ∈ A f ⁡ x ∈ C = f | f Fn x | x ∈ B ∧ ∀ x ∈ B f ⁡ x ∈ C
9 df-ixp ⊢ ⨉ x ∈ A C = f | f Fn x | x ∈ A ∧ ∀ x ∈ A f ⁡ x ∈ C
10 df-ixp ⊢ ⨉ x ∈ B C = f | f Fn x | x ∈ B ∧ ∀ x ∈ B f ⁡ x ∈ C
11 8 9 10 3eqtr4i ⊢ ⨉ x ∈ A C = ⨉ x ∈ B C