Metamath Proof Explorer


Theorem elun2

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

Ref Expression
Assertion elun2 A B A C B

Proof

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