This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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