Metamath Proof Explorer

Theorem ssun

Description: A condition that implies inclusion in the union of two classes. (Contributed by NM, 23-Nov-2003)

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

Proof

Step Hyp Ref Expression
1 ssun3 
 |-  ( A C_ B -> A C_ ( B u. C ) )
2 ssun4 
 |-  ( A C_ C -> A C_ ( B u. C ) )
3 1 2 jaoi 
 |-  ( ( A C_ B \/ A C_ C ) -> A C_ ( B u. C ) )