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 𝐴 = { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 = { 𝑦 } }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1	0	bj-csngl	⊢ sngl 𝐴
2		vx	⊢ 𝑥
3		vy	⊢ 𝑦
4	2	cv	⊢ 𝑥
5	3	cv	⊢ 𝑦
6	5	csn	⊢ { 𝑦 }
7	4 6	wceq	⊢ 𝑥 = { 𝑦 }
8	7 3 0	wrex	⊢ ∃ 𝑦 ∈ 𝐴 𝑥 = { 𝑦 }
9	8 2	cab	⊢ { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 = { 𝑦 } }
10	1 9	wceq	⊢ sngl 𝐴 = { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 = { 𝑦 } }