Metamath Proof Explorer

Theorem xpss12

Description: Subset theorem for Cartesian product. Generalization of Theorem 101 of Suppes p. 52. (Contributed by NM, 26-Aug-1995) (Proof shortened by Andrew Salmon, 27-Aug-2011)

		Ref	Expression
	Assertion	xpss12	$⊢ (A \subseteq B \land C \subseteq D) \to A \times C \subseteq B \times D$

Proof

Step	Hyp	Ref	Expression
1		ssel	$⊢ A \subseteq B \to (x \in A \to x \in B)$
2		ssel	$⊢ C \subseteq D \to (y \in C \to y \in D)$
3	1 2	im2anan9	$⊢ (A \subseteq B \land C \subseteq D) \to ((x \in A \land y \in C) \to (x \in B \land y \in D))$
4	3	ssopab2dv	$⊢ (A \subseteq B \land C \subseteq D) \to \{⟨x, y⟩ \| (x \in A \land y \in C)\} \subseteq \{⟨x, y⟩ \| (x \in B \land y \in D)\}$
5		df-xp	$⊢ A \times C = \{⟨x, y⟩ \| (x \in A \land y \in C)\}$
6		df-xp	$⊢ B \times D = \{⟨x, y⟩ \| (x \in B \land y \in D)\}$
7	4 5 6	3sstr4g	$⊢ (A \subseteq B \land C \subseteq D) \to A \times C \subseteq B \times D$