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 31077
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 31076 . 2  class sngl  A
3 vx . . . . . 6  setvar  x
43cv 1404 . . . . 5  class  x
5 vy . . . . . . 7  setvar  y
65cv 1404 . . . . . 6  class  y
76csn 3971 . . . . 5  class  { y }
84, 7wceq 1405 . . . 4  wff  x  =  { y }
98, 5, 1wrex 2754 . . 3  wff  E. y  e.  A  x  =  { y }
109, 3cab 2387 . 2  class  { x  |  E. y  e.  A  x  =  { y } }
112, 10wceq 1405 1  wff sngl  A  =  { x  |  E. y  e.  A  x  =  { y } }
Colors of variables: wff setvar class
This definition is referenced by:  bj-sngleq  31078  bj-elsngl  31079
  Copyright terms: Public domain W3C validator