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