Theorem bj-snglinv

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

	Ref	Expression
Assertion	bj-snglinv	|- A = { x | { x } e. sngl A }

Proof

Step	Hyp	Ref	Expression
1		bj-snglc	|- ( x e. A <-> { x } e. sngl A )
2	1	abbi2i	|- A = { x | { x } e. sngl A }