# 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 𝐸 = Slot ( 𝐸 ‘ ndx )
setsnid.n ( 𝐸 ‘ ndx ) ≠ 𝐷
Assertion setsnid ( 𝐸𝑊 ) = ( 𝐸 ‘ ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) )

### Proof

Step Hyp Ref Expression
1 setsid.e 𝐸 = Slot ( 𝐸 ‘ ndx )
2 setsnid.n ( 𝐸 ‘ ndx ) ≠ 𝐷
3 id ( 𝑊 ∈ V → 𝑊 ∈ V )
4 1 3 strfvnd ( 𝑊 ∈ V → ( 𝐸𝑊 ) = ( 𝑊 ‘ ( 𝐸 ‘ ndx ) ) )
5 ovex ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ∈ V
6 5 1 strfvn ( 𝐸 ‘ ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ) = ( ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ‘ ( 𝐸 ‘ ndx ) )
7 setsres ( 𝑊 ∈ V → ( ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ↾ ( V ∖ { 𝐷 } ) ) = ( 𝑊 ↾ ( V ∖ { 𝐷 } ) ) )
8 7 fveq1d ( 𝑊 ∈ V → ( ( ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ↾ ( V ∖ { 𝐷 } ) ) ‘ ( 𝐸 ‘ ndx ) ) = ( ( 𝑊 ↾ ( V ∖ { 𝐷 } ) ) ‘ ( 𝐸 ‘ ndx ) ) )
9 fvex ( 𝐸 ‘ ndx ) ∈ V
10 eldifsn ( ( 𝐸 ‘ ndx ) ∈ ( V ∖ { 𝐷 } ) ↔ ( ( 𝐸 ‘ ndx ) ∈ V ∧ ( 𝐸 ‘ ndx ) ≠ 𝐷 ) )
11 9 2 10 mpbir2an ( 𝐸 ‘ ndx ) ∈ ( V ∖ { 𝐷 } )
12 fvres ( ( 𝐸 ‘ ndx ) ∈ ( V ∖ { 𝐷 } ) → ( ( ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ↾ ( V ∖ { 𝐷 } ) ) ‘ ( 𝐸 ‘ ndx ) ) = ( ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ‘ ( 𝐸 ‘ ndx ) ) )
13 11 12 ax-mp ( ( ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ↾ ( V ∖ { 𝐷 } ) ) ‘ ( 𝐸 ‘ ndx ) ) = ( ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ‘ ( 𝐸 ‘ ndx ) )
14 fvres ( ( 𝐸 ‘ ndx ) ∈ ( V ∖ { 𝐷 } ) → ( ( 𝑊 ↾ ( V ∖ { 𝐷 } ) ) ‘ ( 𝐸 ‘ ndx ) ) = ( 𝑊 ‘ ( 𝐸 ‘ ndx ) ) )
15 11 14 ax-mp ( ( 𝑊 ↾ ( V ∖ { 𝐷 } ) ) ‘ ( 𝐸 ‘ ndx ) ) = ( 𝑊 ‘ ( 𝐸 ‘ ndx ) )
16 8 13 15 3eqtr3g ( 𝑊 ∈ V → ( ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ‘ ( 𝐸 ‘ ndx ) ) = ( 𝑊 ‘ ( 𝐸 ‘ ndx ) ) )
17 6 16 syl5eq ( 𝑊 ∈ V → ( 𝐸 ‘ ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ) = ( 𝑊 ‘ ( 𝐸 ‘ ndx ) ) )
18 4 17 eqtr4d ( 𝑊 ∈ V → ( 𝐸𝑊 ) = ( 𝐸 ‘ ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ) )
19 1 str0 ∅ = ( 𝐸 ‘ ∅ )
20 fvprc ( ¬ 𝑊 ∈ V → ( 𝐸𝑊 ) = ∅ )
21 reldmsets Rel dom sSet
22 21 ovprc1 ( ¬ 𝑊 ∈ V → ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) = ∅ )
23 22 fveq2d ( ¬ 𝑊 ∈ V → ( 𝐸 ‘ ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ) = ( 𝐸 ‘ ∅ ) )
24 19 20 23 3eqtr4a ( ¬ 𝑊 ∈ V → ( 𝐸𝑊 ) = ( 𝐸 ‘ ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ) )
25 18 24 pm2.61i ( 𝐸𝑊 ) = ( 𝐸 ‘ ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) )