Theorem dfsingles2

Description: Alternate definition of the class of all singletons. (Contributed by Scott Fenton, 20-Nov-2013) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Assertion	dfsingles2	|- Singletons = { x | E. y x = { y } }

Proof

Step	Hyp	Ref	Expression
1		elsingles	|- ( x e. Singletons <-> E. y x = { y } )
2	1	eqabi	|- Singletons = { x | E. y x = { y } }