Description: A singleton is a set. Theorem 7.12 of Quine p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT . (Contributed by NM, 7-Aug-1994) (Revised by Mario Carneiro, 19-May-2013)
|- { A } e. _V
|- ( A e. _V -> { A } e. _V )
|- ( -. A e. _V <-> { A } = (/) )
|- ( -. A e. _V -> { A } = (/) )
|- (/) e. _V
|- ( -. A e. _V -> { A } e. _V )