Theorem uniss

Description: Subclass relationship for class union. Theorem 61 of Suppes p. 39. (Contributed by NM, 22-Mar-1998) (Proof shortened by Andrew Salmon, 29-Jun-2011)

	Ref	Expression
Assertion	uniss	$$⊢A\subseteq B\to \bigcup A\subseteq \bigcup B$$

Proof

Step	Hyp	Ref	Expression
1		ssel	$$⊢A\subseteq B\to \left(y\in A\to y\in B\right)$$
2	1	anim2d	$$⊢A\subseteq B\to \left(\left(x\in y\wedge y\in A\right)\to \left(x\in y\wedge y\in B\right)\right)$$
3	2	eximdv	$$⊢A\subseteq B\to \left(\exists y\left(x\in y\wedge y\in A\right)\to \exists y\left(x\in y\wedge y\in B\right)\right)$$
4		eluni	$$⊢x\in \bigcup A\leftrightarrow \exists y\left(x\in y\wedge y\in A\right)$$
5		eluni	$$⊢x\in \bigcup B\leftrightarrow \exists y\left(x\in y\wedge y\in B\right)$$
6	3 4 5	3imtr4g	$$⊢A\subseteq B\to \left(x\in \bigcup A\to x\in \bigcup B\right)$$
7	6	ssrdv	$$⊢A\subseteq B\to \bigcup A\subseteq \bigcup B$$