Metamath Proof Explorer

Theorem ixpeq12dv

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

Ref Expression
Hypotheses ixpeq12dv.1 ⊢ φ → A = B
ixpeq12dv.2 ⊢ φ → C = D
Assertion ixpeq12dv ⊢ φ → ⨉ x ∈ A C = ⨉ x ∈ B D

Proof

Step Hyp Ref Expression
1 ixpeq12dv.1 ⊢ φ → A = B
2 ixpeq12dv.2 ⊢ φ → C = D
3 1 eleq2d ⊢ φ → x ∈ A ↔ x ∈ B
4 3 abbidv ⊢ φ → x | x ∈ A = x | x ∈ B
5 4 fneq2d ⊢ φ → t Fn x | x ∈ A ↔ t Fn x | x ∈ B
6 3 imbi1d ⊢ φ → x ∈ A → t ⁡ x ∈ C ↔ x ∈ B → t ⁡ x ∈ C
7 6 albidv ⊢ φ → ∀ x x ∈ A → t ⁡ x ∈ C ↔ ∀ x x ∈ B → t ⁡ x ∈ C
8 df-ral ⊢ ∀ x ∈ A t ⁡ x ∈ C ↔ ∀ x x ∈ A → t ⁡ x ∈ C
9 df-ral ⊢ ∀ x ∈ B t ⁡ x ∈ C ↔ ∀ x x ∈ B → t ⁡ x ∈ C
10 7 8 9 3bitr4g ⊢ φ → ∀ x ∈ A t ⁡ x ∈ C ↔ ∀ x ∈ B t ⁡ x ∈ C
11 5 10 anbi12d ⊢ φ → t Fn x | x ∈ A ∧ ∀ x ∈ A t ⁡ x ∈ C ↔ t Fn x | x ∈ B ∧ ∀ x ∈ B t ⁡ x ∈ C
12 11 abbidv ⊢ φ → t | t Fn x | x ∈ A ∧ ∀ x ∈ A t ⁡ x ∈ C = t | t Fn x | x ∈ B ∧ ∀ x ∈ B t ⁡ x ∈ C
13 df-ixp ⊢ ⨉ x ∈ A C = t | t Fn x | x ∈ A ∧ ∀ x ∈ A t ⁡ x ∈ C
14 df-ixp ⊢ ⨉ x ∈ B C = t | t Fn x | x ∈ B ∧ ∀ x ∈ B t ⁡ x ∈ C
15 12 13 14 3eqtr4g ⊢ φ → ⨉ x ∈ A C = ⨉ x ∈ B C
16 2 ixpeq2dv ⊢ φ → ⨉ x ∈ B C = ⨉ x ∈ B D
17 15 16 eqtrd ⊢ φ → ⨉ x ∈ A C = ⨉ x ∈ B D