Definition df-singles

Description: Define the class of all singletons. See elsingles for membership. (Contributed by Scott Fenton, 19-Feb-2013)

	Ref	Expression
Assertion	df-singles	|- Singletons = ran Singleton

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csingles	|- Singletons
1		csingle	|- Singleton
2	1	crn	|- ran Singleton
3	0 2	wceq	|- Singletons = ran Singleton