Metamath Proof Explorer

Theorem ixpeq2

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

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

Proof

Step Hyp Ref Expression
1 ss2ixp ⊢ ∀ x ∈ A B ⊆ C → ⨉ x ∈ A B ⊆ ⨉ x ∈ A C
2 ss2ixp ⊢ ∀ x ∈ A C ⊆ B → ⨉ x ∈ A C ⊆ ⨉ x ∈ A B
3 1 2 anim12i ⊢ ∀ x ∈ A B ⊆ C ∧ ∀ x ∈ A C ⊆ B → ⨉ x ∈ A B ⊆ ⨉ x ∈ A C ∧ ⨉ x ∈ A C ⊆ ⨉ x ∈ A B
4 eqss ⊢ B = C ↔ B ⊆ C ∧ C ⊆ B
5 4 ralbii ⊢ ∀ x ∈ A B = C ↔ ∀ x ∈ A B ⊆ C ∧ C ⊆ B
6 r19.26 ⊢ ∀ x ∈ A B ⊆ C ∧ C ⊆ B ↔ ∀ x ∈ A B ⊆ C ∧ ∀ x ∈ A C ⊆ B
7 5 6 bitri ⊢ ∀ x ∈ A B = C ↔ ∀ x ∈ A B ⊆ C ∧ ∀ x ∈ A C ⊆ B
8 eqss ⊢ ⨉ x ∈ A B = ⨉ x ∈ A C ↔ ⨉ x ∈ A B ⊆ ⨉ x ∈ A C ∧ ⨉ x ∈ A C ⊆ ⨉ x ∈ A B
9 3 7 8 3imtr4i ⊢ ∀ x ∈ A B = C → ⨉ x ∈ A B = ⨉ x ∈ A C