Metamath Proof Explorer


Theorem elun1

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

Ref Expression
Assertion elun1 ABABC

Proof

Step Hyp Ref Expression
1 ssun1 BBC
2 1 sseli ABABC