Metamath Proof Explorer


Theorem bj-snglinv

Description: Inverse of singletonization. (Contributed by BJ, 6-Oct-2018)

Ref Expression
Assertion bj-snglinv 𝐴 = { 𝑥 ∣ { 𝑥 } ∈ sngl 𝐴 }

Proof

Step Hyp Ref Expression
1 bj-snglc ( 𝑥𝐴 ↔ { 𝑥 } ∈ sngl 𝐴 )
2 1 abbi2i 𝐴 = { 𝑥 ∣ { 𝑥 } ∈ sngl 𝐴 }