Metamath Proof Explorer

Theorem ssun1

Description: Subclass relationship for union of classes. Theorem 25 of Suppes p. 27. (Contributed by NM, 5-Aug-1993)

Ref Expression
Assertion ssun1 A A B


Step Hyp Ref Expression
1 orc x A x A x B
2 elun x A B x A x B
3 1 2 sylibr x A x A B
4 3 ssriv A A B