Metamath Proof Explorer


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 | y A x = y

Detailed syntax breakdown

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