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 A C
unssi.2 B C
Assertion unssi A B C


Step Hyp Ref Expression
1 unssi.1 A C
2 unssi.2 B C
3 1 2 pm3.2i A C B C
4 unss A C B C A B C
5 3 4 mpbi A B C