# Metamath Proof Explorer

## Theorem altxpeq2

Description: Equality for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012)

Ref Expression
Assertion altxpeq2 ${⊢}{A}={B}\to \left({C}\mathrm{××}{A}\right)=\left({C}\mathrm{××}{B}\right)$

### Proof

Step Hyp Ref Expression
1 rexeq ${⊢}{A}={B}\to \left(\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}=⟪{x},{y}⟫↔\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}=⟪{x},{y}⟫\right)$
2 1 rexbidv ${⊢}{A}={B}\to \left(\exists {x}\in {C}\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}=⟪{x},{y}⟫↔\exists {x}\in {C}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}=⟪{x},{y}⟫\right)$
3 2 abbidv ${⊢}{A}={B}\to \left\{{z}|\exists {x}\in {C}\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}=⟪{x},{y}⟫\right\}=\left\{{z}|\exists {x}\in {C}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}=⟪{x},{y}⟫\right\}$
4 df-altxp ${⊢}\left({C}\mathrm{××}{A}\right)=\left\{{z}|\exists {x}\in {C}\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}=⟪{x},{y}⟫\right\}$
5 df-altxp ${⊢}\left({C}\mathrm{××}{B}\right)=\left\{{z}|\exists {x}\in {C}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}=⟪{x},{y}⟫\right\}$
6 3 4 5 3eqtr4g ${⊢}{A}={B}\to \left({C}\mathrm{××}{A}\right)=\left({C}\mathrm{××}{B}\right)$