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	$$⊢snglA=\left\{x|\exists y\in Ax=\left\{y\right\}\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1	0	bj-csngl	$$classsnglA$$
2		vx	$$setvarx$$
3		vy	$$setvary$$
4	2	cv	$$setvarx$$
5	3	cv	$$setvary$$
6	5	csn	$$class\left\{y\right\}$$
7	4 6	wceq	$$wffx=\left\{y\right\}$$
8	7 3 0	wrex	$$wff\exists y\in Ax=\left\{y\right\}$$
9	8 2	cab	$$class\left\{x|\exists y\in Ax=\left\{y\right\}\right\}$$
10	1 9	wceq	$$wffsnglA=\left\{x|\exists y\in Ax=\left\{y\right\}\right\}$$