Definition df-sets 11966

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 11967 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 = (𝑠 ∈ V, 𝑒 ∈ V ↦ ((𝑠 ↾ (V ∖ dom {𝑒})) ∪ {𝑒}))

Distinct variable group:   𝑒,𝑠

Detailed syntax breakdown of Definition df-sets

Step	Hyp	Ref	Expression
1		csts 11957	. 2 class sSet
2		vs	. . 3 setvar 𝑠
3		ve	. . 3 setvar 𝑒
4		cvv 2686	. . 3 class V
5	2	cv 1330	. . . . 5 class 𝑠
6	3	cv 1330	. . . . . . . 8 class 𝑒
7	6	csn 3527	. . . . . . 7 class {𝑒}
8	7	cdm 4539	. . . . . 6 class dom {𝑒}
9	4, 8	cdif 3068	. . . . 5 class (V ∖ dom {𝑒})
10	5, 9	cres 4541	. . . 4 class (𝑠 ↾ (V ∖ dom {𝑒}))
11	10, 7	cun 3069	. . 3 class ((𝑠 ↾ (V ∖ dom {𝑒})) ∪ {𝑒})
12	2, 3, 4, 4, 11	cmpo 5776	. 2 class (𝑠 ∈ V, 𝑒 ∈ V ↦ ((𝑠 ↾ (V ∖ dom {𝑒})) ∪ {𝑒}))
13	1, 12	wceq 1331	1 wff sSet = (𝑠 ∈ V, 𝑒 ∈ V ↦ ((𝑠 ↾ (V ∖ dom {𝑒})) ∪ {𝑒}))

This definition is referenced by:  reldmsets  11988  setsvalg  11989