Theorem setsidvald

Description: Value of the structure replacement function, deduction version.

Hint: Do not substitute N by a specific (positive) integer to be independent of a hard-coded index value. Often, ( Endx ) can be used instead of N . (Contributed by AV, 14-Mar-2020) (Revised by AV, 17-Oct-2024)

	Ref	Expression
Hypotheses	setsidvald.e	⊢ 𝐸 = Slot 𝑁
	setsidvald.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
	setsidvald.f	⊢ ( 𝜑 → Fun 𝑆 )
	setsidvald.d	⊢ ( 𝜑 → 𝑁 ∈ dom 𝑆 )
Assertion	setsidvald	⊢ ( 𝜑 → 𝑆 = ( 𝑆 sSet ⟨ 𝑁 , ( 𝐸 ‘ 𝑆 ) ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		setsidvald.e	⊢ 𝐸 = Slot 𝑁
2		setsidvald.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
3		setsidvald.f	⊢ ( 𝜑 → Fun 𝑆 )
4		setsidvald.d	⊢ ( 𝜑 → 𝑁 ∈ dom 𝑆 )
5		fvex	⊢ ( 𝐸 ‘ 𝑆 ) ∈ V
6		setsval	⊢ ( ( 𝑆 ∈ 𝑉 ∧ ( 𝐸 ‘ 𝑆 ) ∈ V ) → ( 𝑆 sSet ⟨ 𝑁 , ( 𝐸 ‘ 𝑆 ) ⟩ ) = ( ( 𝑆 ↾ ( V ∖ { 𝑁 } ) ) ∪ { ⟨ 𝑁 , ( 𝐸 ‘ 𝑆 ) ⟩ } ) )
7	2 5 6	sylancl	⊢ ( 𝜑 → ( 𝑆 sSet ⟨ 𝑁 , ( 𝐸 ‘ 𝑆 ) ⟩ ) = ( ( 𝑆 ↾ ( V ∖ { 𝑁 } ) ) ∪ { ⟨ 𝑁 , ( 𝐸 ‘ 𝑆 ) ⟩ } ) )
8	1 2	strfvnd	⊢ ( 𝜑 → ( 𝐸 ‘ 𝑆 ) = ( 𝑆 ‘ 𝑁 ) )
9	8	opeq2d	⊢ ( 𝜑 → ⟨ 𝑁 , ( 𝐸 ‘ 𝑆 ) ⟩ = ⟨ 𝑁 , ( 𝑆 ‘ 𝑁 ) ⟩ )
10	9	sneqd	⊢ ( 𝜑 → { ⟨ 𝑁 , ( 𝐸 ‘ 𝑆 ) ⟩ } = { ⟨ 𝑁 , ( 𝑆 ‘ 𝑁 ) ⟩ } )
11	10	uneq2d	⊢ ( 𝜑 → ( ( 𝑆 ↾ ( V ∖ { 𝑁 } ) ) ∪ { ⟨ 𝑁 , ( 𝐸 ‘ 𝑆 ) ⟩ } ) = ( ( 𝑆 ↾ ( V ∖ { 𝑁 } ) ) ∪ { ⟨ 𝑁 , ( 𝑆 ‘ 𝑁 ) ⟩ } ) )
12		funresdfunsn	⊢ ( ( Fun 𝑆 ∧ 𝑁 ∈ dom 𝑆 ) → ( ( 𝑆 ↾ ( V ∖ { 𝑁 } ) ) ∪ { ⟨ 𝑁 , ( 𝑆 ‘ 𝑁 ) ⟩ } ) = 𝑆 )
13	3 4 12	syl2anc	⊢ ( 𝜑 → ( ( 𝑆 ↾ ( V ∖ { 𝑁 } ) ) ∪ { ⟨ 𝑁 , ( 𝑆 ‘ 𝑁 ) ⟩ } ) = 𝑆 )
14	7 11 13	3eqtrrd	⊢ ( 𝜑 → 𝑆 = ( 𝑆 sSet ⟨ 𝑁 , ( 𝐸 ‘ 𝑆 ) ⟩ ) )