Theorem unssi

Description: An inference showing the union of two subclasses is a subclass. (Contributed by Raph Levien, 10-Dec-2002)

	Ref	Expression
Hypotheses	unssi.1	$$⊢A\subseteq C$$
	unssi.2	$$⊢B\subseteq C$$
Assertion	unssi	$$⊢A\cup B\subseteq C$$

Proof

Step	Hyp	Ref	Expression
1		unssi.1	$$⊢A\subseteq C$$
2		unssi.2	$$⊢B\subseteq C$$
3	1 2	pm3.2i	$$⊢\left(A\subseteq C\wedge B\subseteq C\right)$$
4		unss	$$⊢\left(A\subseteq C\wedge B\subseteq C\right)\leftrightarrow A\cup B\subseteq C$$
5	3 4	mpbi	$$⊢A\cup B\subseteq C$$