Definition df-bj-sngl 32954

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

Assertion

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

Distinct variable group:   x, y, A

Detailed syntax breakdown of Definition df-bj-sngl

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	bj-csngl 32953	. 2 class sngl A
3		vx	. . . . . 6 setvar x
4	3	cv 1482	. . . . 5 class x
5		vy	. . . . . . 7 setvar y
6	5	cv 1482	. . . . . 6 class y
7	6	csn 4177	. . . . 5 class { y }
8	4, 7	wceq 1483	. . . 4 wff x = { y }
9	8, 5, 1	wrex 2913	. . 3 wff E. y e. A x = { y }
10	9, 3	cab 2608	. 2 class { x | E. y e. A x = { y } }
11	2, 10	wceq 1483	1 wff sngl A = { x | E. y e. A x = { y } }

This definition is referenced by:  bj-sngleq  32955  bj-elsngl  32956