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

Definition df-sset 30448
Description: Define the subset class. For the value, see brsset 30482. (Contributed by Scott Fenton, 31-Mar-2012.)
Assertion
Ref Expression
df-sset  |-  SSet  =  ( ( _V  X.  _V )  \  ran  (  _E  (x)  ( _V  \  _E  ) ) )

Detailed syntax breakdown of Definition df-sset
StepHypRef Expression
1 csset 30424 . 2  class  SSet
2 cvv 3078 . . . 4  class  _V
32, 2cxp 4843 . . 3  class  ( _V 
X.  _V )
4 cep 4754 . . . . 5  class  _E
52, 4cdif 3430 . . . . 5  class  ( _V 
\  _E  )
64, 5ctxp 30422 . . . 4  class  (  _E 
(x)  ( _V  \  _E  ) )
76crn 4846 . . 3  class  ran  (  _E  (x)  ( _V  \  _E  ) )
83, 7cdif 3430 . 2  class  ( ( _V  X.  _V )  \  ran  (  _E  (x)  ( _V  \  _E  )
) )
91, 8wceq 1437 1  wff  SSet  =  ( ( _V  X.  _V )  \  ran  (  _E  (x)  ( _V  \  _E  ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  relsset  30481  brsset  30482
  Copyright terms: Public domain W3C validator