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

Metamath Proof Explorer

Theorem xpss2

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

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

Step	Hyp	Ref	Expression
1		ssid	$⊢ C \subseteq C$
2		xpss12	$⊢ (C \subseteq C \land A \subseteq B) \to C \times A \subseteq C \times B$
3	1 2	mpan	$⊢ A \subseteq B \to C \times A \subseteq C \times B$