Metamath Proof Explorer


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

Proof

Step Hyp Ref Expression
1 elsingles x 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 y x = y
2 1 abbi2i 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 = x | y x = y