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

Metamath Proof Explorer

Theorem xpss

Description: A Cartesian product is included in the ordered pair universe. Exercise 3 of TakeutiZaring p. 25. (Contributed by NM, 2-Aug-1994)

		Ref	Expression
	Assertion	xpss	$⊢ A \times B \subseteq V \times V$

Step	Hyp	Ref	Expression
1		ssv	$⊢ A \subseteq V$
2		ssv	$⊢ B \subseteq V$
3		xpss12	$⊢ (A \subseteq V \land B \subseteq V) \to A \times B \subseteq V \times V$
4	1 2 3	mp2an	$⊢ A \times B \subseteq V \times V$