Theorem snex

Description: A singleton is a set. Theorem 7.12 of Quine p. 51, proved using Extensionality, Separation and Pairing. See also snexALT . (Contributed by NM, 7-Aug-1994) (Revised by Mario Carneiro, 19-May-2013) Avoid ax-nul and shorten proof. (Revised by GG, 6-Mar-2026)

	Ref	Expression
Assertion	snex	|- { A } e. _V

Proof

Step	Hyp	Ref	Expression
1		dfsn2	|- { A } = { A , A }
2		prex	|- { A , A } e. _V
3	1 2	eqeltri	|- { A } e. _V