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	$$⊢\left[B/A\right.]sS=\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\left(\mathrm{ndx}\right)\right\}\right)}\right)\cup \left\{⟨A\left(\mathrm{ndx}\right),B⟩\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cB	$$classB$$
1		cA	$$classA$$
2		cS	$$classS$$
3	1 0 2	cstrset	$$class\left[B/A\right.]sS$$
4		cvv	$$class\mathrm{V}$$
5		cnx	$$class\mathrm{ndx}$$
6	5 1	cfv	$$classA\left(\mathrm{ndx}\right)$$
7	6	csn	$$class\left\{A\left(\mathrm{ndx}\right)\right\}$$
8	4 7	cdif	$$class\left(\mathrm{V}\setminus \left\{A\left(\mathrm{ndx}\right)\right\}\right)$$
9	2 8	cres	$$class\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\left(\mathrm{ndx}\right)\right\}\right)}\right)$$
10	6 0	cop	$$class⟨A\left(\mathrm{ndx}\right),B⟩$$
11	10	csn	$$class\left\{⟨A\left(\mathrm{ndx}\right),B⟩\right\}$$
12	9 11	cun	$$class\left(\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\left(\mathrm{ndx}\right)\right\}\right)}\right)\cup \left\{⟨A\left(\mathrm{ndx}\right),B⟩\right\}\right)$$
13	3 12	wceq	$$wff\left[B/A\right.]sS=\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\left(\mathrm{ndx}\right)\right\}\right)}\right)\cup \left\{⟨A\left(\mathrm{ndx}\right),B⟩\right\}$$