Definition df-strset 34455

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

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cS	. . 3 class 𝑆
4	1, 2, 3	cstrset 34454	. 2 class [𝐵 / 𝐴]struct𝑆
5		cvv 3491	. . . . 5 class V
6		cnx 16473	. . . . . . 7 class ndx
7	6, 1	cfv 6348	. . . . . 6 class (𝐴‘ndx)
8	7	csn 4560	. . . . 5 class {(𝐴‘ndx)}
9	5, 8	cdif 3926	. . . 4 class (V ∖ {(𝐴‘ndx)})
10	3, 9	cres 5550	. . 3 class (𝑆 ↾ (V ∖ {(𝐴‘ndx)}))
11	7, 2	cop 4566	. . . 4 class ⟨(𝐴‘ndx), 𝐵⟩
12	11	csn 4560	. . 3 class {⟨(𝐴‘ndx), 𝐵⟩}
13	10, 12	cun 3927	. 2 class ((𝑆 ↾ (V ∖ {(𝐴‘ndx)})) ∪ {⟨(𝐴‘ndx), 𝐵⟩})
14	4, 13	wceq 1536	1 wff [𝐵 / 𝐴]struct𝑆 = ((𝑆 ↾ (V ∖ {(𝐴‘ndx)})) ∪ {⟨(𝐴‘ndx), 𝐵⟩})

This definition is referenced by:  setsstrset  34456