Theorem setsidvald

Description: Value of the structure replacement function, deduction version. (Contributed by AV, 14-Mar-2020)

	Ref	Expression
Hypotheses	setsidvald.e	|- E = Slot N
	setsidvald.n	|- N e. NN
	setsidvald.s	|- ( ph -> S e. V )
	setsidvald.f	|- ( ph -> Fun S )
	setsidvald.d	|- ( ph -> ( E ` ndx ) e. dom S )
Assertion	setsidvald	|- ( ph -> S = ( S sSet <. ( E ` ndx ) , ( E ` S ) >. ) )

Proof

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