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

Metamath Proof Explorer

Theorem ssiun2

Description: Identity law for subset of an indexed union. (Contributed by NM, 12-Oct-2003) (Proof shortened by Andrew Salmon, 25-Jul-2011)

		Ref	Expression
	Assertion	ssiun2	$⊢ x \in A \to B \subseteq ⋃_{x \in A} B$

Step	Hyp	Ref	Expression
1		rspe	$⊢ (x \in A \land y \in B) \to \exists x \in A y \in B$
2	1	ex	$⊢ x \in A \to (y \in B \to \exists x \in A y \in B)$
3		eliun	$⊢ y \in ⋃_{x \in A} B \leftrightarrow \exists x \in A y \in B$
4	2 3	imbitrrdi	$⊢ x \in A \to (y \in B \to y \in ⋃_{x \in A} B)$
5	4	ssrdv	$⊢ x \in A \to B \subseteq ⋃_{x \in A} B$