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