Metamath Proof Explorer

Theorem unss1

Description: Subclass law for union of classes. (Contributed by NM, 14-Oct-1999) (Proof shortened by Andrew Salmon, 26-Jun-2011)

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

Proof

Step Hyp Ref Expression
1 ssel 
 |-  ( A C_ B -> ( x e. A -> x e. B ) )
2 1 orim1d 
 |-  ( A C_ B -> ( ( x e. A \/ x e. C ) -> ( x e. B \/ x e. C ) ) )
3 elun 
 |-  ( x e. ( A u. C ) <-> ( x e. A \/ x e. C ) )
4 elun 
 |-  ( x e. ( B u. C ) <-> ( x e. B \/ x e. C ) )
5 2 3 4 3imtr4g 
 |-  ( A C_ B -> ( x e. ( A u. C ) -> x e. ( B u. C ) ) )
6 5 ssrdv 
 |-  ( A C_ B -> ( A u. C ) C_ ( B u. C ) )