Theorem bj-snglinv

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

	Ref	Expression
Assertion	bj-snglinv	$$⊢A=\left\{x|\left\{x\right\}\in snglA\right\}$$

Proof

Step	Hyp	Ref	Expression
1		bj-snglc	$$⊢x\in A\leftrightarrow \left\{x\right\}\in snglA$$
2	1	eqabi	$$⊢A=\left\{x|\left\{x\right\}\in snglA\right\}$$