Metamath Proof Explorer

Theorem unss2

Description: Subclass law for union of classes. Exercise 7 of TakeutiZaring p. 18. (Contributed by NM, 14-Oct-1999)

Ref Expression
Assertion unss2 
|- ( A C_ B -> ( C u. A ) C_ ( C u. B ) )

Proof

Step Hyp Ref Expression
1 unss1 
 |-  ( A C_ B -> ( A u. C ) C_ ( B u. C ) )
2 uncom 
 |-  ( C u. A ) = ( A u. C )
3 uncom 
 |-  ( C u. B ) = ( B u. C )
4 1 2 3 3sstr4g 
 |-  ( A C_ B -> ( C u. A ) C_ ( C u. B ) )