Definition df-sets 12469

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-iress 12470 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

Step	Hyp	Ref	Expression
1		csts 12460	. 2 class sSet
2		vs	. . 3 setvar s
3		ve	. . 3 setvar e
4		cvv 2738	. . 3 class _V
5	2	cv 1352	. . . . 5 class s
6	3	cv 1352	. . . . . . . 8 class e
7	6	csn 3593	. . . . . . 7 class { e }
8	7	cdm 4627	. . . . . 6 class dom { e }
9	4, 8	cdif 3127	. . . . 5 class ( _V \ dom { e } )
10	5, 9	cres 4629	. . . 4 class ( s |` ( _V \ dom { e } ) )
11	10, 7	cun 3128	. . 3 class ( ( s |` ( _V \ dom { e } ) ) u. { e } )
12	2, 3, 4, 4, 11	cmpo 5877	. 2 class ( s e. _V , e e. _V |-> ( ( s |` ( _V \ dom { e } ) ) u. { e } ) )
13	1, 12	wceq 1353	1 wff sSet = ( s e. _V , e e. _V |-> ( ( s |` ( _V \ dom { e } ) ) u. { e } ) )

This definition is referenced by:  reldmsets  12491  setsvalg  12492