Theorem unissi

Description: Subclass relationship for subclass union. Inference form of uniss . (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypothesis	unissi.1	$$⊢A\subseteq B$$
Assertion	unissi	$$⊢\bigcup A\subseteq \bigcup B$$

Proof

Step	Hyp	Ref	Expression
1		unissi.1	$$⊢A\subseteq B$$
2		uniss	$$⊢A\subseteq B\to \bigcup A\subseteq \bigcup B$$
3	1 2	ax-mp	$$⊢\bigcup A\subseteq \bigcup B$$