Metamath Proof Explorer

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 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 = ran 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇

Detailed syntax breakdown

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