This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \| \exists y x = \{y\}\}$

Proof

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