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