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 C_ C
	unssi.2	|- B C_ C
Assertion	unssi	|- ( A u. B ) C_ C

Proof

Step	Hyp	Ref	Expression
1		unssi.1	|- A C_ C
2		unssi.2	|- B C_ C
3	1 2	pm3.2i	|- ( A C_ C /\ B C_ C )
4		unss	|- ( ( A C_ C /\ B C_ C ) <-> ( A u. B ) C_ C )
5	3 4	mpbi	|- ( A u. B ) C_ C