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 \bigcup _{x\in A}B$$

Proof

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