This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xpdom1

Description: Dominance law for Cartesian product. Theorem 6L(c) of Enderton p. 149. (Contributed by NM, 28-Sep-2004) (Revised by NM, 29-Mar-2006) (Revised by Mario Carneiro, 7-May-2015)

		Ref	Expression
	Hypothesis	xpdom1.2	$⊢ C \in V$
	Assertion	xpdom1	$⊢ A ≼ B \to (A \times C) ≼ (B \times C)$

Proof

Step	Hyp	Ref	Expression
1		xpdom1.2	$⊢ C \in V$
2		xpdom1g	$⊢ (C \in V \land A ≼ B) \to (A \times C) ≼ (B \times C)$
3	1 2	mpan	$⊢ A ≼ B \to (A \times C) ≼ (B \times C)$