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	$$⊢\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}=\left\{x|\exists yx=\left\{y\right\}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		elsingles	$$⊢x\in \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}\leftrightarrow \exists yx=\left\{y\right\}$$
2	1	eqabi	$$⊢\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}=\left\{x|\exists yx=\left\{y\right\}\right\}$$