Metamath Proof Explorer

Theorem snssd

Description: The singleton of an element of a class is a subset of the class (deduction form). (Contributed by Jonathan Ben-Naim, 3-Jun-2011)

Ref Expression
Hypothesis snssd.1 φ A B
Assertion snssd φ A B


Step Hyp Ref Expression
1 snssd.1 φ A B
2 snssi A B A B
3 1 2 syl φ A B