Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bj-sngl Structured version   Visualization version   GIF version

Definition df-bj-sngl 34397
Description: Definition of "singletonization". The class sngl 𝐴 is isomorphic to 𝐴 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.)
Assertion
Ref Expression
df-bj-sngl sngl 𝐴 = {𝑥 ∣ ∃𝑦𝐴 𝑥 = {𝑦}}
Distinct variable group:   𝑥,𝑦,𝐴

Detailed syntax breakdown of Definition df-bj-sngl
StepHypRef Expression
1 cA . . 3 class 𝐴
21bj-csngl 34396 . 2 class sngl 𝐴
3 vx . . . . . 6 setvar 𝑥
43cv 1537 . . . . 5 class 𝑥
5 vy . . . . . . 7 setvar 𝑦
65cv 1537 . . . . . 6 class 𝑦
76csn 4528 . . . . 5 class {𝑦}
84, 7wceq 1538 . . . 4 wff 𝑥 = {𝑦}
98, 5, 1wrex 3110 . . 3 wff 𝑦𝐴 𝑥 = {𝑦}
109, 3cab 2779 . 2 class {𝑥 ∣ ∃𝑦𝐴 𝑥 = {𝑦}}
112, 10wceq 1538 1 wff sngl 𝐴 = {𝑥 ∣ ∃𝑦𝐴 𝑥 = {𝑦}}
Colors of variables: wff setvar class
This definition is referenced by:  bj-sngleq  34398  bj-elsngl  34399
  Copyright terms: Public domain W3C validator