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 e. B -> { A } C_ B )

Proof

Step Hyp Ref Expression
1 snssg 
 |-  ( A e. B -> ( A e. B <-> { A } C_ B ) )
2 1 ibi 
 |-  ( A e. B -> { A } C_ B )