Metamath Proof Explorer

Theorem elun1

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

Ref Expression
Assertion elun1 
|- ( A e. B -> A e. ( B u. C ) )

Proof

Step Hyp Ref Expression
1 ssun1 
 |-  B C_ ( B u. C )
2 1 sseli 
 |-  ( A e. B -> A e. ( B u. C ) )