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 e. _V |
|
| Assertion | snss | |- ( A e. B <-> { A } C_ B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | snss.1 | |- A e. _V |
|
| 2 | snssg | |- ( A e. _V -> ( A e. B <-> { A } C_ B ) ) |
|
| 3 | 1 2 | ax-mp | |- ( A e. B <-> { A } C_ B ) |