Metamath Proof Explorer

Theorem elun2

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

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

Proof

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