Metamath Proof Explorer

Theorem unss12

Description: Subclass law for union of classes. (Contributed by NM, 2-Jun-2004)

Ref Expression
Assertion unss12 
|- ( ( A C_ B /\ C C_ D ) -> ( A u. C ) C_ ( B u. D ) )

Proof

Step Hyp Ref Expression
1 unss1 
 |-  ( A C_ B -> ( A u. C ) C_ ( B u. C ) )
2 unss2 
 |-  ( C C_ D -> ( B u. C ) C_ ( B u. D ) )
3 1 2 sylan9ss 
 |-  ( ( A C_ B /\ C C_ D ) -> ( A u. C ) C_ ( B u. D ) )