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 34551
 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 34550 . 2 class [𝐵 / 𝐴]struct𝑆
5 cvv 3444 . . . . 5 class V
6 cnx 16476 . . . . . . 7 class ndx
76, 1cfv 6328 . . . . . 6 class (𝐴‘ndx)
87csn 4528 . . . . 5 class {(𝐴‘ndx)}
95, 8cdif 3881 . . . 4 class (V ∖ {(𝐴‘ndx)})
103, 9cres 5525 . . 3 class (𝑆 ↾ (V ∖ {(𝐴‘ndx)}))
117, 2cop 4534 . . . 4 class ⟨(𝐴‘ndx), 𝐵
1211csn 4528 . . 3 class {⟨(𝐴‘ndx), 𝐵⟩}
1310, 12cun 3882 . 2 class ((𝑆 ↾ (V ∖ {(𝐴‘ndx)})) ∪ {⟨(𝐴‘ndx), 𝐵⟩})
144, 13wceq 1538 1 wff [𝐵 / 𝐴]struct𝑆 = ((𝑆 ↾ (V ∖ {(𝐴‘ndx)})) ∪ {⟨(𝐴‘ndx), 𝐵⟩})
 Colors of variables: wff setvar class This definition is referenced by:  setsstrset  34552
 Copyright terms: Public domain W3C validator