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

Proof

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