xpeq2

Description: Equality theorem for Cartesian product. (Contributed by NM, 5-Jul-1994)

		Ref	Expression
	Assertion	xpeq2	$⊢ A = B \to C \times A = C \times B$

Step	Hyp	Ref	Expression
1		eleq2	$⊢ A = B \to (y \in A \leftrightarrow y \in B)$
2	1	anbi2d	$⊢ A = B \to ((x \in C \land y \in A) \leftrightarrow (x \in C \land y \in B))$
3	2	opabbidv	$⊢ A = B \to \{⟨x, y⟩ \| (x \in C \land y \in A)\} = \{⟨x, y⟩ \| (x \in C \land y \in B)\}$
4		df-xp	$⊢ C \times A = \{⟨x, y⟩ \| (x \in C \land y \in A)\}$
5		df-xp	$⊢ C \times B = \{⟨x, y⟩ \| (x \in C \land y \in B)\}$
6	3 4 5	3eqtr4g	$⊢ A = B \to C \times A = C \times B$

Metamath Proof Explorer