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

Proof

Step	Hyp	Ref	Expression
1		unssd.1	|- ( ph -> A C_ C )
2		unssd.2	|- ( ph -> B C_ C )
3		unss	|- ( ( A C_ C /\ B C_ C ) <-> ( A u. B ) C_ C )
4	3	biimpi	|- ( ( A C_ C /\ B C_ C ) -> ( A u. B ) C_ C )
5	1 2 4	syl2anc	|- ( ph -> ( A u. B ) C_ C )