Metamath Proof Explorer

Theorem ssun3

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

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

Proof

Step Hyp Ref Expression
1 ssun1 
 |-  B C_ ( B u. C )
2 sstr2 
 |-  ( A C_ B -> ( B C_ ( B u. C ) -> A C_ ( B u. C ) ) )
3 1 2 mpi 
 |-  ( A C_ B -> A C_ ( B u. C ) )