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