Definition df-bj-sngl

Description: Definition of "singletonization". The class sngl A is isomorphic to A and since it contains only singletons, it can be easily be adjoined disjoint elements, which can be useful in various constructions. (Contributed by BJ, 6-Oct-2018)

	Ref	Expression
Assertion	df-bj-sngl	|- sngl A = { x | E. y e. A x = { y } }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1	0	bj-csngl	|- sngl A
2		vx	|- x
3		vy	|- y
4	2	cv	|- x
5	3	cv	|- y
6	5	csn	|- { y }
7	4 6	wceq	|- x = { y }
8	7 3 0	wrex	|- E. y e. A x = { y }
9	8 2	cab	|- { x | E. y e. A x = { y } }
10	1 9	wceq	|- sngl A = { x | E. y e. A x = { y } }