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


Step Hyp Ref Expression
1 snssg A B A B A B
2 1 ibi A B A B