# Metamath Proof Explorer

## Theorem ixpeq2

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

Ref Expression
Assertion ixpeq2 ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}={C}\to \underset{{x}\in {A}}{⨉}{B}=\underset{{x}\in {A}}{⨉}{C}$

### Proof

Step Hyp Ref Expression
1 ss2ixp ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\subseteq {C}\to \underset{{x}\in {A}}{⨉}{B}\subseteq \underset{{x}\in {A}}{⨉}{C}$
2 ss2ixp ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{C}\subseteq {B}\to \underset{{x}\in {A}}{⨉}{C}\subseteq \underset{{x}\in {A}}{⨉}{B}$
3 1 2 anim12i ${⊢}\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\subseteq {C}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{C}\subseteq {B}\right)\to \left(\underset{{x}\in {A}}{⨉}{B}\subseteq \underset{{x}\in {A}}{⨉}{C}\wedge \underset{{x}\in {A}}{⨉}{C}\subseteq \underset{{x}\in {A}}{⨉}{B}\right)$
4 eqss ${⊢}{B}={C}↔\left({B}\subseteq {C}\wedge {C}\subseteq {B}\right)$
5 4 ralbii ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}={C}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {C}\wedge {C}\subseteq {B}\right)$
6 r19.26 ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {C}\wedge {C}\subseteq {B}\right)↔\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\subseteq {C}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{C}\subseteq {B}\right)$
7 5 6 bitri ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}={C}↔\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\subseteq {C}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{C}\subseteq {B}\right)$
8 eqss ${⊢}\underset{{x}\in {A}}{⨉}{B}=\underset{{x}\in {A}}{⨉}{C}↔\left(\underset{{x}\in {A}}{⨉}{B}\subseteq \underset{{x}\in {A}}{⨉}{C}\wedge \underset{{x}\in {A}}{⨉}{C}\subseteq \underset{{x}\in {A}}{⨉}{B}\right)$
9 3 7 8 3imtr4i ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}={C}\to \underset{{x}\in {A}}{⨉}{B}=\underset{{x}\in {A}}{⨉}{C}$