Metamath Proof Explorer

Theorem ssun2

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

Ref Expression
Assertion ssun2 
|- A C_ ( B u. A )

Proof

Step Hyp Ref Expression
1 ssun1 
 |-  A C_ ( A u. B )
2 uncom 
 |-  ( A u. B ) = ( B u. A )
3 1 2 sseqtri 
 |-  A C_ ( B u. A )