Theorem xpss1

Description: Subset relation for Cartesian product. (Contributed by Jeff Hankins, 30-Aug-2009)

	Ref	Expression
Assertion	xpss1	$$⊢A\subseteq B\to A\times C\subseteq B\times C$$

Proof

Step	Hyp	Ref	Expression
1		ssid	$$⊢C\subseteq C$$
2		xpss12	$$⊢\left(A\subseteq B\wedge C\subseteq C\right)\to A\times C\subseteq B\times C$$
3	1 2	mpan2	$$⊢A\subseteq B\to A\times C\subseteq B\times C$$