Metamath Proof Explorer


Theorem elun1

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

Ref Expression
Assertion elun1 A B A B C

Proof

Step Hyp Ref Expression
1 ssun1 B B C
2 1 sseli A B A B C