Theorem unssd

Description: A deduction showing the union of two subclasses is a subclass. (Contributed by Jonathan Ben-Naim, 3-Jun-2011)

	Ref	Expression
Hypotheses	unssd.1	$$⊢\phi \to A\subseteq C$$
	unssd.2	$$⊢\phi \to B\subseteq C$$
Assertion	unssd	$$⊢\phi \to A\cup B\subseteq C$$

Proof

Step	Hyp	Ref	Expression
1		unssd.1	$$⊢\phi \to A\subseteq C$$
2		unssd.2	$$⊢\phi \to B\subseteq C$$
3		unss	$$⊢\left(A\subseteq C\wedge B\subseteq C\right)\leftrightarrow A\cup B\subseteq C$$
4	3	biimpi	$$⊢\left(A\subseteq C\wedge B\subseteq C\right)\to A\cup B\subseteq C$$
5	1 2 4	syl2anc	$$⊢\phi \to A\cup B\subseteq C$$