Theorem snelsingles

Description: A singleton is a member of the class of all singletons. (Contributed by Scott Fenton, 19-Feb-2013)

	Ref	Expression
Hypothesis	snelsingles.1	|- A e. _V
Assertion	snelsingles	|- { A } e. Singletons

Proof

Step	Hyp	Ref	Expression
1		snelsingles.1	|- A e. _V
2		isset	|- ( A e. _V <-> E. x x = A )
3		eqcom	|- ( x = A <-> A = x )
4	3	exbii	|- ( E. x x = A <-> E. x A = x )
5	2 4	bitri	|- ( A e. _V <-> E. x A = x )
6	1 5	mpbi	|- E. x A = x
7		sneq	|- ( A = x -> { A } = { x } )
8	6 7	eximii	|- E. x { A } = { x }
9		elsingles	|- ( { A } e. Singletons <-> E. x { A } = { x } )
10	8 9	mpbir	|- { A } e. Singletons