Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-strset Structured version   Visualization version   GIF version

Definition df-strset 33420
Description: Component-setting in extensible structures. Define the extensible structure [𝐵 / 𝐴]struct𝑆, which is like the extensible structure 𝑆 except that the value 𝐵 has been put in the slot 𝐴 (replacing the current value if there was already one). In such expressions, 𝐴 is generally substituted for slot mnemonics like Base or +g or dist. (Contributed by BJ, 13-Feb-2022.)
Assertion
Ref Expression
df-strset [𝐵 / 𝐴]struct𝑆 = ((𝑆 ↾ (V ∖ {(𝐴‘ndx)})) ∪ {⟨(𝐴‘ndx), 𝐵⟩})

Detailed syntax breakdown of Definition df-strset
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 cS . . 3 class 𝑆
41, 2, 3cstrset 33419 . 2 class [𝐵 / 𝐴]struct𝑆
5 cvv 3351 . . . . 5 class V
6 cnx 16061 . . . . . . 7 class ndx
76, 1cfv 6031 . . . . . 6 class (𝐴‘ndx)
87csn 4316 . . . . 5 class {(𝐴‘ndx)}
95, 8cdif 3720 . . . 4 class (V ∖ {(𝐴‘ndx)})
103, 9cres 5251 . . 3 class (𝑆 ↾ (V ∖ {(𝐴‘ndx)}))
117, 2cop 4322 . . . 4 class ⟨(𝐴‘ndx), 𝐵
1211csn 4316 . . 3 class {⟨(𝐴‘ndx), 𝐵⟩}
1310, 12cun 3721 . 2 class ((𝑆 ↾ (V ∖ {(𝐴‘ndx)})) ∪ {⟨(𝐴‘ndx), 𝐵⟩})
144, 13wceq 1631 1 wff [𝐵 / 𝐴]struct𝑆 = ((𝑆 ↾ (V ∖ {(𝐴‘ndx)})) ∪ {⟨(𝐴‘ndx), 𝐵⟩})
Colors of variables: wff setvar class
This definition is referenced by:  setsstrset  33421
  Copyright terms: Public domain W3C validator