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 \mathrm{V}$$
Assertion	xpdom1	$$⊢A\preccurlyeq B\to \left(A\times C\right)\preccurlyeq \left(B\times C\right)$$

Proof

Step	Hyp	Ref	Expression
1		xpdom1.2	$$⊢C\in \mathrm{V}$$
2		xpdom1g	$$⊢\left(C\in \mathrm{V}\wedge A\preccurlyeq B\right)\to \left(A\times C\right)\preccurlyeq \left(B\times C\right)$$
3	1 2	mpan	$$⊢A\preccurlyeq B\to \left(A\times C\right)\preccurlyeq \left(B\times C\right)$$