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	⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
	unssd.2	⊢ ( 𝜑 → 𝐵 ⊆ 𝐶 )
Assertion	unssd	⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) ⊆ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		unssd.1	⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
2		unssd.2	⊢ ( 𝜑 → 𝐵 ⊆ 𝐶 )
3		unss	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) ↔ ( 𝐴 ∪ 𝐵 ) ⊆ 𝐶 )
4	3	biimpi	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝐴 ∪ 𝐵 ) ⊆ 𝐶 )
5	1 2 4	syl2anc	⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) ⊆ 𝐶 )