ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-sets Unicode version

Definition df-sets 11955
Description: Set a component of an extensible structure. This function is useful for taking an existing structure and "overriding" one of its components. For example, df-ress 11956 adjusts the base set to match its second argument, which has the effect of making subgroups, subspaces, subrings etc. from the original structures. (Contributed by Mario Carneiro, 1-Dec-2014.)
Assertion
Ref Expression
df-sets  |- sSet  =  ( s  e.  _V , 
e  e.  _V  |->  ( ( s  |`  ( _V  \  dom  { e } ) )  u. 
{ e } ) )
Distinct variable group:    e, s

Detailed syntax breakdown of Definition df-sets
StepHypRef Expression
1 csts 11946 . 2  class sSet
2 vs . . 3  setvar  s
3 ve . . 3  setvar  e
4 cvv 2681 . . 3  class  _V
52cv 1330 . . . . 5  class  s
63cv 1330 . . . . . . . 8  class  e
76csn 3522 . . . . . . 7  class  { e }
87cdm 4534 . . . . . 6  class  dom  {
e }
94, 8cdif 3063 . . . . 5  class  ( _V 
\  dom  { e } )
105, 9cres 4536 . . . 4  class  ( s  |`  ( _V  \  dom  { e } ) )
1110, 7cun 3064 . . 3  class  ( ( s  |`  ( _V  \  dom  { e } ) )  u.  {
e } )
122, 3, 4, 4, 11cmpo 5769 . 2  class  ( s  e.  _V ,  e  e.  _V  |->  ( ( s  |`  ( _V  \  dom  { e } ) )  u.  {
e } ) )
131, 12wceq 1331 1  wff sSet  =  ( s  e.  _V , 
e  e.  _V  |->  ( ( s  |`  ( _V  \  dom  { e } ) )  u. 
{ e } ) )
Colors of variables: wff set class
This definition is referenced by:  reldmsets  11977  setsvalg  11978
  Copyright terms: Public domain W3C validator