Metamath Proof Explorer


Theorem elun2

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

Ref Expression
Assertion elun2 ABACB

Proof

Step Hyp Ref Expression
1 ssun2 BCB
2 1 sseli ABACB