Metamath Proof Explorer

Theorem ixpeq2

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

Ref Expression
Assertion ixpeq2 ⊢∀x∈AB=C→⨉x∈AB=⨉x∈AC

Proof

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