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	|- E = Slot N
	setsidvald.s	|- ( ph -> S e. V )
	setsidvald.f	|- ( ph -> Fun S )
	setsidvald.d	|- ( ph -> N e. dom S )
Assertion	setsidvald	|- ( ph -> S = ( S sSet <. N , ( E ` S ) >. ) )

Proof

Step	Hyp	Ref	Expression
1		setsidvald.e	|- E = Slot N
2		setsidvald.s	|- ( ph -> S e. V )
3		setsidvald.f	|- ( ph -> Fun S )
4		setsidvald.d	|- ( ph -> N e. dom S )
5		fvex	|- ( E ` S ) e. _V
6		setsval	|- ( ( S e. V /\ ( E ` S ) e. _V ) -> ( S sSet <. N , ( E ` S ) >. ) = ( ( S |` ( _V \ { N } ) ) u. { <. N , ( E ` S ) >. } ) )
7	2 5 6	sylancl	|- ( ph -> ( S sSet <. N , ( E ` S ) >. ) = ( ( S |` ( _V \ { N } ) ) u. { <. N , ( E ` S ) >. } ) )
8	1 2	strfvnd	|- ( ph -> ( E ` S ) = ( S ` N ) )
9	8	opeq2d	|- ( ph -> <. N , ( E ` S ) >. = <. N , ( S ` N ) >. )
10	9	sneqd	|- ( ph -> { <. N , ( E ` S ) >. } = { <. N , ( S ` N ) >. } )
11	10	uneq2d	|- ( ph -> ( ( S |` ( _V \ { N } ) ) u. { <. N , ( E ` S ) >. } ) = ( ( S |` ( _V \ { N } ) ) u. { <. N , ( S ` N ) >. } ) )
12		funresdfunsn	|- ( ( Fun S /\ N e. dom S ) -> ( ( S |` ( _V \ { N } ) ) u. { <. N , ( S ` N ) >. } ) = S )
13	3 4 12	syl2anc	|- ( ph -> ( ( S |` ( _V \ { N } ) ) u. { <. N , ( S ` N ) >. } ) = S )
14	7 11 13	3eqtrrd	|- ( ph -> S = ( S sSet <. N , ( E ` S ) >. ) )