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	eqabi	⊢ 𝐴 = { 𝑥 ∣ { 𝑥 } ∈ sngl 𝐴 }