This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem snex

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)

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

Proof

Step	Hyp	Ref	Expression
1		snexg	\|- ( A e. _V -> { A } e. _V )
2		snprc	\|- ( -. A e. _V <-> { A } = (/) )
3	2	biimpi	\|- ( -. A e. _V -> { A } = (/) )
4		0ex	\|- (/) e. _V
5	3 4	eqeltrdi	\|- ( -. A e. _V -> { A } e. _V )
6	1 5	pm2.61i	\|- { A } e. _V