Theorem unissd

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

	Ref	Expression
Hypothesis	unissd.1	$$⊢\phi \to A\subseteq B$$
Assertion	unissd	$$⊢\phi \to \bigcup A\subseteq \bigcup B$$

Proof

Step	Hyp	Ref	Expression
1		unissd.1	$$⊢\phi \to A\subseteq B$$
2		uniss	$$⊢A\subseteq B\to \bigcup A\subseteq \bigcup B$$
3	1 2	syl	$$⊢\phi \to \bigcup A\subseteq \bigcup B$$