Theorem setsstrset

Description: Relation between df-sets and df-strset . Temporary theorem kept during the transition from the former to the latter. (Contributed by BJ, 13-Feb-2022)

	Ref	Expression
Assertion	setsstrset	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → [ 𝐵 / 𝐴 ]struct 𝑆 = ( 𝑆 sSet ⟨ ( 𝐴 ‘ ndx ) , 𝐵 ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		df-strset	⊢ [ 𝐵 / 𝐴 ]struct 𝑆 = ( ( 𝑆 ↾ ( V ∖ { ( 𝐴 ‘ ndx ) } ) ) ∪ { ⟨ ( 𝐴 ‘ ndx ) , 𝐵 ⟩ } )
2		setsval	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑆 sSet ⟨ ( 𝐴 ‘ ndx ) , 𝐵 ⟩ ) = ( ( 𝑆 ↾ ( V ∖ { ( 𝐴 ‘ ndx ) } ) ) ∪ { ⟨ ( 𝐴 ‘ ndx ) , 𝐵 ⟩ } ) )
3	1 2	eqtr4id	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → [ 𝐵 / 𝐴 ]struct 𝑆 = ( 𝑆 sSet ⟨ ( 𝐴 ‘ ndx ) , 𝐵 ⟩ ) )