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

Definition df-sets 11666
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 11667 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
StepHypRef Expression
1 csts 11657 . 2 class sSet
2 vs . . 3 setvar 𝑠
3 ve . . 3 setvar 𝑒
4 cvv 2633 . . 3 class V
52cv 1295 . . . . 5 class 𝑠
63cv 1295 . . . . . . . 8 class 𝑒
76csn 3466 . . . . . . 7 class {𝑒}
87cdm 4467 . . . . . 6 class dom {𝑒}
94, 8cdif 3010 . . . . 5 class (V ∖ dom {𝑒})
105, 9cres 4469 . . . 4 class (𝑠 ↾ (V ∖ dom {𝑒}))
1110, 7cun 3011 . . 3 class ((𝑠 ↾ (V ∖ dom {𝑒})) ∪ {𝑒})
122, 3, 4, 4, 11cmpt2 5692 . 2 class (𝑠 ∈ V, 𝑒 ∈ V ↦ ((𝑠 ↾ (V ∖ dom {𝑒})) ∪ {𝑒}))
131, 12wceq 1296 1 wff sSet = (𝑠 ∈ V, 𝑒 ∈ V ↦ ((𝑠 ↾ (V ∖ dom {𝑒})) ∪ {𝑒}))
Colors of variables: wff set class
This definition is referenced by:  reldmsets  11688  setsvalg  11689
  Copyright terms: Public domain W3C validator