Metamath Proof Explorer

Theorem snss

Description: The singleton of an element of a class is a subset of the class (inference form of snssg ). Theorem 7.4 of Quine p. 49. (Contributed by NM, 21-Jun-1993)

Ref Expression
Hypothesis snss.1 A V
Assertion snss A B A B


Step Hyp Ref Expression
1 snss.1 A V
2 snssg A V A B A B
3 1 2 ax-mp A B A B