Theorem setsnid 17244

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.) (Proof shortened by AV, 7-Nov-2024.)

Hypotheses

Ref	Expression
setsid.e	⊢ 𝐸 = Slot (𝐸‘ndx)
setsnid.n	⊢ (𝐸‘ndx) ≠ 𝐷

Assertion

Ref	Expression
setsnid	⊢ (𝐸‘𝑊) = (𝐸‘(𝑊 sSet ⟨𝐷, 𝐶⟩))

Proof of Theorem setsnid

Step	Hyp	Ref	Expression
1		setsid.e	. . . 4 ⊢ 𝐸 = Slot (𝐸‘ndx)
2		id 22	. . . 4 ⊢ (𝑊 ∈ V → 𝑊 ∈ V)
3	1, 2	strfvnd 17221	. . 3 ⊢ (𝑊 ∈ V → (𝐸‘𝑊) = (𝑊‘(𝐸‘ndx)))
4		ovex 7429	. . . . 5 ⊢ (𝑊 sSet ⟨𝐷, 𝐶⟩) ∈ V
5	4, 1	strfvn 17222	. . . 4 ⊢ (𝐸‘(𝑊 sSet ⟨𝐷, 𝐶⟩)) = ((𝑊 sSet ⟨𝐷, 𝐶⟩)‘(𝐸‘ndx))
6		setsres 17214	. . . . . 6 ⊢ (𝑊 ∈ V → ((𝑊 sSet ⟨𝐷, 𝐶⟩) ↾ (V ∖ {𝐷})) = (𝑊 ↾ (V ∖ {𝐷})))
7	6	fveq1d 6869	. . . . 5 ⊢ (𝑊 ∈ V → (((𝑊 sSet ⟨𝐷, 𝐶⟩) ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = ((𝑊 ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)))
8		fvex 6880	. . . . . . 7 ⊢ (𝐸‘ndx) ∈ V
9		setsnid.n	. . . . . . 7 ⊢ (𝐸‘ndx) ≠ 𝐷
10		eldifsn 4746	. . . . . . 7 ⊢ ((𝐸‘ndx) ∈ (V ∖ {𝐷}) ↔ ((𝐸‘ndx) ∈ V ∧ (𝐸‘ndx) ≠ 𝐷))
11	8, 9, 10	mpbir2an 721	. . . . . 6 ⊢ (𝐸‘ndx) ∈ (V ∖ {𝐷})
12		fvres 6886	. . . . . 6 ⊢ ((𝐸‘ndx) ∈ (V ∖ {𝐷}) → (((𝑊 sSet ⟨𝐷, 𝐶⟩) ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = ((𝑊 sSet ⟨𝐷, 𝐶⟩)‘(𝐸‘ndx)))
13	11, 12	ax-mp 5	. . . . 5 ⊢ (((𝑊 sSet ⟨𝐷, 𝐶⟩) ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = ((𝑊 sSet ⟨𝐷, 𝐶⟩)‘(𝐸‘ndx))
14		fvres 6886	. . . . . 6 ⊢ ((𝐸‘ndx) ∈ (V ∖ {𝐷}) → ((𝑊 ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = (𝑊‘(𝐸‘ndx)))
15	11, 14	ax-mp 5	. . . . 5 ⊢ ((𝑊 ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = (𝑊‘(𝐸‘ndx))
16	7, 13, 15	3eqtr3g 2820	. . . 4 ⊢ (𝑊 ∈ V → ((𝑊 sSet ⟨𝐷, 𝐶⟩)‘(𝐸‘ndx)) = (𝑊‘(𝐸‘ndx)))
17	5, 16	eqtrid 2809	. . 3 ⊢ (𝑊 ∈ V → (𝐸‘(𝑊 sSet ⟨𝐷, 𝐶⟩)) = (𝑊‘(𝐸‘ndx)))
18	3, 17	eqtr4d 2800	. 2 ⊢ (𝑊 ∈ V → (𝐸‘𝑊) = (𝐸‘(𝑊 sSet ⟨𝐷, 𝐶⟩)))
19	1	str0 17225	. . . 4 ⊢ ∅ = (𝐸‘∅)
20	19	eqcomi 2771	. . 3 ⊢ (𝐸‘∅) = ∅
21		eqid 2762	. . 3 ⊢ (𝑊 sSet ⟨𝐷, 𝐶⟩) = (𝑊 sSet ⟨𝐷, 𝐶⟩)
22		reldmsets 17201	. . 3 ⊢ Rel dom sSet
23	20, 21, 22	oveqprc 17228	. 2 ⊢ (¬ 𝑊 ∈ V → (𝐸‘𝑊) = (𝐸‘(𝑊 sSet ⟨𝐷, 𝐶⟩)))
24	18, 23	pm2.61i 183	1 ⊢ (𝐸‘𝑊) = (𝐸‘(𝑊 sSet ⟨𝐷, 𝐶⟩))

Syntax hints:   = wceq 1560   ∈ wcel 2142   ≠ wne 2957  Vcvv 3454   ∖ cdif 3901  ∅c0 4285  {csn 4582  ⟨cop 4588   ↾ cres 5649  ‘cfv 6521  (class class class)co 7396   sSet csts 17199  Slot cslot 17217  ndxcnx 17229

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pr 5390  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-sbc 3745  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-res 5659  df-iota 6477  df-fun 6523  df-fv 6529  df-ov 7399  df-oprab 7400  df-mpo 7401  df-sets 17200  df-slot 17218

This theorem is referenced by:  resseqnbas  17278  oppchomfval  17746  oppcbas  17750  rescbas  17862  rescco  17865  rescabs  17866  odubas  18323  setsplusg  19390  opprlem  20391  rmodislmod  20997  sralem  21243  srasca  21247  sravsca  21248  zlmlem  21568  zlmsca  21572  znbaslem  21590  thlbas  21748  thlle  21749  opsrbaslem  22102  matbas  22473  matplusg  22474  matsca  22475  matvsca  22476  tuslem  24326  setsmsbas  24535  setsmsds  24536  tnglem  24700  tngds  24708  ttgval  29075  ttglem  29076  cchhllem  29087  setsvtx  29236  resvlem  33519  zlmds  34259  zlmtset  34260  hlhilslem  42562  mnringnmulrd  44790  cznrnglem  48881  cznabel  48882  cznrng  48883  prstcnidlem  50173  prstcnid  50174