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	$$⊢\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}=\mathrm{ran}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csingles	$$class\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}$$
1		csingle	$$class\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}$$
2	1	crn	$$class\mathrm{ran}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}$$
3	0 2	wceq	$$wff\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}=\mathrm{ran}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}$$