# Metamath Proof Explorer

## Theorem setsnid

Description: Value of the structure replacement function at an untouched index. (Contributed by Mario Carneiro, 1-Dec-2014) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Hypotheses setsid.e
`|- E = Slot ( E ` ndx )`
setsnid.n
`|- ( E ` ndx ) =/= D`
Assertion setsnid
`|- ( E ` W ) = ( E ` ( W sSet <. D , C >. ) )`

### Proof

Step Hyp Ref Expression
1 setsid.e
` |-  E = Slot ( E ` ndx )`
2 setsnid.n
` |-  ( E ` ndx ) =/= D`
3 id
` |-  ( W e. _V -> W e. _V )`
4 1 3 strfvnd
` |-  ( W e. _V -> ( E ` W ) = ( W ` ( E ` ndx ) ) )`
5 ovex
` |-  ( W sSet <. D , C >. ) e. _V`
6 5 1 strfvn
` |-  ( E ` ( W sSet <. D , C >. ) ) = ( ( W sSet <. D , C >. ) ` ( E ` ndx ) )`
7 setsres
` |-  ( W e. _V -> ( ( W sSet <. D , C >. ) |` ( _V \ { D } ) ) = ( W |` ( _V \ { D } ) ) )`
8 7 fveq1d
` |-  ( W e. _V -> ( ( ( W sSet <. D , C >. ) |` ( _V \ { D } ) ) ` ( E ` ndx ) ) = ( ( W |` ( _V \ { D } ) ) ` ( E ` ndx ) ) )`
9 fvex
` |-  ( E ` ndx ) e. _V`
10 eldifsn
` |-  ( ( E ` ndx ) e. ( _V \ { D } ) <-> ( ( E ` ndx ) e. _V /\ ( E ` ndx ) =/= D ) )`
11 9 2 10 mpbir2an
` |-  ( E ` ndx ) e. ( _V \ { D } )`
12 fvres
` |-  ( ( E ` ndx ) e. ( _V \ { D } ) -> ( ( ( W sSet <. D , C >. ) |` ( _V \ { D } ) ) ` ( E ` ndx ) ) = ( ( W sSet <. D , C >. ) ` ( E ` ndx ) ) )`
13 11 12 ax-mp
` |-  ( ( ( W sSet <. D , C >. ) |` ( _V \ { D } ) ) ` ( E ` ndx ) ) = ( ( W sSet <. D , C >. ) ` ( E ` ndx ) )`
14 fvres
` |-  ( ( E ` ndx ) e. ( _V \ { D } ) -> ( ( W |` ( _V \ { D } ) ) ` ( E ` ndx ) ) = ( W ` ( E ` ndx ) ) )`
15 11 14 ax-mp
` |-  ( ( W |` ( _V \ { D } ) ) ` ( E ` ndx ) ) = ( W ` ( E ` ndx ) )`
16 8 13 15 3eqtr3g
` |-  ( W e. _V -> ( ( W sSet <. D , C >. ) ` ( E ` ndx ) ) = ( W ` ( E ` ndx ) ) )`
17 6 16 syl5eq
` |-  ( W e. _V -> ( E ` ( W sSet <. D , C >. ) ) = ( W ` ( E ` ndx ) ) )`
18 4 17 eqtr4d
` |-  ( W e. _V -> ( E ` W ) = ( E ` ( W sSet <. D , C >. ) ) )`
19 1 str0
` |-  (/) = ( E ` (/) )`
20 fvprc
` |-  ( -. W e. _V -> ( E ` W ) = (/) )`
21 reldmsets
` |-  Rel dom sSet`
22 21 ovprc1
` |-  ( -. W e. _V -> ( W sSet <. D , C >. ) = (/) )`
23 22 fveq2d
` |-  ( -. W e. _V -> ( E ` ( W sSet <. D , C >. ) ) = ( E ` (/) ) )`
24 19 20 23 3eqtr4a
` |-  ( -. W e. _V -> ( E ` W ) = ( E ` ( W sSet <. D , C >. ) ) )`
25 18 24 pm2.61i
` |-  ( E ` W ) = ( E ` ( W sSet <. D , C >. ) )`