Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-singleton Structured version   Unicode version

Definition df-singleton 29486
Description: Define the singleton function. See brsingle 29542 for its value. (Contributed by Scott Fenton, 4-Apr-2014.)
Assertion
Ref Expression
df-singleton  |- Singleton  =  ( ( _V  X.  _V )  \  ran  ( ( _V  (x)  _E  )(++) (  _I  (x)  _V )
) )

Detailed syntax breakdown of Definition df-singleton
StepHypRef Expression
1 csingle 29462 . 2  class Singleton
2 cvv 3095 . . . 4  class  _V
32, 2cxp 4987 . . 3  class  ( _V 
X.  _V )
4 cep 4779 . . . . . 6  class  _E
52, 4ctxp 29454 . . . . 5  class  ( _V 
(x)  _E  )
6 cid 4780 . . . . . 6  class  _I
76, 2ctxp 29454 . . . . 5  class  (  _I 
(x)  _V )
85, 7csymdif 29442 . . . 4  class  ( ( _V  (x)  _E  )(++) (  _I  (x)  _V )
)
98crn 4990 . . 3  class  ran  (
( _V  (x)  _E  )(++) (  _I  (x)  _V ) )
103, 9cdif 3458 . 2  class  ( ( _V  X.  _V )  \  ran  ( ( _V 
(x)  _E  )(++) (  _I  (x)  _V ) ) )
111, 10wceq 1383 1  wff Singleton  =  ( ( _V  X.  _V )  \  ran  ( ( _V  (x)  _E  )(++) (  _I  (x)  _V )
) )
Colors of variables: wff setvar class
This definition is referenced by:  brsingle  29542  fnsingle  29544
  Copyright terms: Public domain W3C validator