Metamath Proof Explorer


Theorem ssun2

Description: Subclass relationship for union of classes. (Contributed by NM, 30-Aug-1993)

Ref Expression
Assertion ssun2 A B A

Proof

Step Hyp Ref Expression
1 ssun1 A A B
2 uncom A B = B A
3 1 2 sseqtri A B A