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

Metamath Proof Explorer

Theorem djussxp

Description: Disjoint union is a subset of a Cartesian product. (Contributed by Stefan O'Rear, 21-Nov-2014)

		Ref	Expression
	Assertion	djussxp	$⊢ ⋃_{x \in A} (\{x\} \times B) \subseteq A \times V$

Step	Hyp	Ref	Expression
1		iunss	$⊢ ⋃_{x \in A} (\{x\} \times B) \subseteq A \times V \leftrightarrow \forall x \in A \{x\} \times B \subseteq A \times V$
2		snssi	$⊢ x \in A \to \{x\} \subseteq A$
3		ssv	$⊢ B \subseteq V$
4		xpss12	$⊢ (\{x\} \subseteq A \land B \subseteq V) \to \{x\} \times B \subseteq A \times V$
5	2 3 4	sylancl	$⊢ x \in A \to \{x\} \times B \subseteq A \times V$
6	1 5	mprgbir	$⊢ ⋃_{x \in A} (\{x\} \times B) \subseteq A \times V$