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	⊢ Singletons = { 𝑥 ∣ ∃ 𝑦 𝑥 = { 𝑦 } }

Proof

Step	Hyp	Ref	Expression
1		elsingles	⊢ ( 𝑥 ∈ Singletons ↔ ∃ 𝑦 𝑥 = { 𝑦 } )
2	1	eqabi	⊢ Singletons = { 𝑥 ∣ ∃ 𝑦 𝑥 = { 𝑦 } }