Metamath Proof Explorer


Theorem snssi

Description: The singleton of an element of a class is a subset of the class. (Contributed by NM, 6-Jun-1994)

Ref Expression
Assertion snssi ⊢ A ∈ B → A ⊆ B

Proof

Step Hyp Ref Expression
1 snssg ⊢ A ∈ B → A ∈ B ↔ A ⊆ B
2 1 ibi ⊢ A ∈ B → A ⊆ B