Metamath Proof Explorer


Definition df-strset

Description: Component-setting in extensible structures. Define the extensible structure [s B / A ]s S , which is like the extensible structure S except that the value B has been put in the slot A (replacing the current value if there was already one). In such expressions, A is generally substituted for slot mnemonics like Base or +g or dist . The _V in this definition was chosen to be closer to df-sets , but since extensible structures are functions on NN , it will be more natural to replace it with NN when df-strset becomes the main definition. (Contributed by BJ, 13-Feb-2022)

Ref Expression
Assertion df-strset B A S = S V A ndx A ndx B

Detailed syntax breakdown

Step Hyp Ref Expression
0 cB class B
1 cA class A
2 cS class S
3 1 0 2 cstrset class B A S
4 cvv class V
5 cnx class ndx
6 5 1 cfv class A ndx
7 6 csn class A ndx
8 4 7 cdif class V A ndx
9 2 8 cres class S V A ndx
10 6 0 cop class A ndx B
11 10 csn class A ndx B
12 9 11 cun class S V A ndx A ndx B
13 3 12 wceq wff B A S = S V A ndx A ndx B