Metamath Proof Explorer

Theorem ssun4

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

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

Proof

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