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

Definition df-bj-sngl 32776
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
StepHypRef Expression
1 cA . . 3  class  A
21bj-csngl 32775 . 2  class sngl  A
3 vx . . . . . 6  setvar  x
43cv 1369 . . . . 5  class  x
5 vy . . . . . . 7  setvar  y
65cv 1369 . . . . . 6  class  y
76csn 3984 . . . . 5  class  { y }
84, 7wceq 1370 . . . 4  wff  x  =  { y }
98, 5, 1wrex 2799 . . 3  wff  E. y  e.  A  x  =  { y }
109, 3cab 2439 . 2  class  { x  |  E. y  e.  A  x  =  { y } }
112, 10wceq 1370 1  wff sngl  A  =  { x  |  E. y  e.  A  x  =  { y } }
Colors of variables: wff setvar class
This definition is referenced by:  bj-sngleq  32777  bj-elsngl  32778
  Copyright terms: Public domain W3C validator