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

Proof

Step	Hyp	Ref	Expression
1		unssi.1	⊢ 𝐴 ⊆ 𝐶
2		unssi.2	⊢ 𝐵 ⊆ 𝐶
3	1 2	pm3.2i	⊢ ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 )
4		unss	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) ↔ ( 𝐴 ∪ 𝐵 ) ⊆ 𝐶 )
5	3 4	mpbi	⊢ ( 𝐴 ∪ 𝐵 ) ⊆ 𝐶