Metamath Proof Explorer

Theorem ssun1

Description: Subclass relationship for union of classes. Theorem 25 of Suppes p. 27. (Contributed by NM, 5-Aug-1993)

Ref Expression
Assertion ssun1 
|- A C_ ( A u. B )

Proof

Step Hyp Ref Expression
1 orc 
 |-  ( x e. A -> ( x e. A \/ x e. B ) )
2 elun 
 |-  ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
3 1 2 sylibr 
 |-  ( x e. A -> x e. ( A u. B ) )
4 3 ssriv 
 |-  A C_ ( A u. B )