Theorem altxpeq1

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

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

Proof

Step	Hyp	Ref	Expression
1		rexeq	$$⊢A=B\to \left(\exists x\in A\exists y\in Cz=⟪x,y⟫\leftrightarrow \exists x\in B\exists y\in Cz=⟪x,y⟫\right)$$
2	1	abbidv	$$⊢A=B\to \left\{z|\exists x\in A\exists y\in Cz=⟪x,y⟫\right\}=\left\{z|\exists x\in B\exists y\in Cz=⟪x,y⟫\right\}$$
3		df-altxp	$$⊢\left(A\mathrm{\times \times }C\right)=\left\{z|\exists x\in A\exists y\in Cz=⟪x,y⟫\right\}$$
4		df-altxp	$$⊢\left(B\mathrm{\times \times }C\right)=\left\{z|\exists x\in B\exists y\in Cz=⟪x,y⟫\right\}$$
5	2 3 4	3eqtr4g	$$⊢A=B\to \left(A\mathrm{\times \times }C\right)=\left(B\mathrm{\times \times }C\right)$$