Description: Inverse of singletonization. (Contributed by BJ, 6-Oct-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | bj-snglinv | ⊢ 𝐴 = { 𝑥 ∣ { 𝑥 } ∈ sngl 𝐴 } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-snglc | ⊢ ( 𝑥 ∈ 𝐴 ↔ { 𝑥 } ∈ sngl 𝐴 ) | |
2 | 1 | abbi2i | ⊢ 𝐴 = { 𝑥 ∣ { 𝑥 } ∈ sngl 𝐴 } |