Theorem unss2

Description: Subclass law for union of classes. Exercise 7 of TakeutiZaring p. 18. (Contributed by NM, 14-Oct-1999)

	Ref	Expression
Assertion	unss2	$$⊢A\subseteq B\to C\cup A\subseteq C\cup B$$

Proof

Step	Hyp	Ref	Expression
1		unss1	$$⊢A\subseteq B\to A\cup C\subseteq B\cup C$$
2		uncom	$$⊢C\cup A=A\cup C$$
3		uncom	$$⊢C\cup B=B\cup C$$
4	1 2 3	3sstr4g	$$⊢A\subseteq B\to C\cup A\subseteq C\cup B$$