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 ABAB

Proof

Step Hyp Ref Expression
1 snssg ABABAB
2 1 ibi ABAB