Theorem setsnid 17245

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 17222	. . 3 ⊢ (𝑊 ∈ V → (𝐸‘𝑊) = (𝑊‘(𝐸‘ndx)))
4		ovex 7464	. . . . 5 ⊢ (𝑊 sSet ⟨𝐷, 𝐶⟩) ∈ V
5	4, 1	strfvn 17223	. . . 4 ⊢ (𝐸‘(𝑊 sSet ⟨𝐷, 𝐶⟩)) = ((𝑊 sSet ⟨𝐷, 𝐶⟩)‘(𝐸‘ndx))
6		setsres 17215	. . . . . 6 ⊢ (𝑊 ∈ V → ((𝑊 sSet ⟨𝐷, 𝐶⟩) ↾ (V ∖ {𝐷})) = (𝑊 ↾ (V ∖ {𝐷})))
7	6	fveq1d 6908	. . . . 5 ⊢ (𝑊 ∈ V → (((𝑊 sSet ⟨𝐷, 𝐶⟩) ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = ((𝑊 ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)))
8		fvex 6919	. . . . . . 7 ⊢ (𝐸‘ndx) ∈ V
9		setsnid.n	. . . . . . 7 ⊢ (𝐸‘ndx) ≠ 𝐷
10		eldifsn 4786	. . . . . . 7 ⊢ ((𝐸‘ndx) ∈ (V ∖ {𝐷}) ↔ ((𝐸‘ndx) ∈ V ∧ (𝐸‘ndx) ≠ 𝐷))
11	8, 9, 10	mpbir2an 711	. . . . . 6 ⊢ (𝐸‘ndx) ∈ (V ∖ {𝐷})
12		fvres 6925	. . . . . 6 ⊢ ((𝐸‘ndx) ∈ (V ∖ {𝐷}) → (((𝑊 sSet ⟨𝐷, 𝐶⟩) ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = ((𝑊 sSet ⟨𝐷, 𝐶⟩)‘(𝐸‘ndx)))
13	11, 12	ax-mp 5	. . . . 5 ⊢ (((𝑊 sSet ⟨𝐷, 𝐶⟩) ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = ((𝑊 sSet ⟨𝐷, 𝐶⟩)‘(𝐸‘ndx))
14		fvres 6925	. . . . . 6 ⊢ ((𝐸‘ndx) ∈ (V ∖ {𝐷}) → ((𝑊 ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = (𝑊‘(𝐸‘ndx)))
15	11, 14	ax-mp 5	. . . . 5 ⊢ ((𝑊 ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = (𝑊‘(𝐸‘ndx))
16	7, 13, 15	3eqtr3g 2800	. . . 4 ⊢ (𝑊 ∈ V → ((𝑊 sSet ⟨𝐷, 𝐶⟩)‘(𝐸‘ndx)) = (𝑊‘(𝐸‘ndx)))
17	5, 16	eqtrid 2789	. . 3 ⊢ (𝑊 ∈ V → (𝐸‘(𝑊 sSet ⟨𝐷, 𝐶⟩)) = (𝑊‘(𝐸‘ndx)))
18	3, 17	eqtr4d 2780	. 2 ⊢ (𝑊 ∈ V → (𝐸‘𝑊) = (𝐸‘(𝑊 sSet ⟨𝐷, 𝐶⟩)))
19	1	str0 17226	. . . 4 ⊢ ∅ = (𝐸‘∅)
20	19	eqcomi 2746	. . 3 ⊢ (𝐸‘∅) = ∅
21		eqid 2737	. . 3 ⊢ (𝑊 sSet ⟨𝐷, 𝐶⟩) = (𝑊 sSet ⟨𝐷, 𝐶⟩)
22		reldmsets 17202	. . 3 ⊢ Rel dom sSet
23	20, 21, 22	oveqprc 17229	. 2 ⊢ (¬ 𝑊 ∈ V → (𝐸‘𝑊) = (𝐸‘(𝑊 sSet ⟨𝐷, 𝐶⟩)))
24	18, 23	pm2.61i 182	1 ⊢ (𝐸‘𝑊) = (𝐸‘(𝑊 sSet ⟨𝐷, 𝐶⟩))

Syntax hints:   = wceq 1540   ∈ wcel 2108   ≠ wne 2940  Vcvv 3480   ∖ cdif 3948  ∅c0 4333  {csn 4626  ⟨cop 4632   ↾ cres 5687  ‘cfv 6561  (class class class)co 7431   sSet csts 17200  Slot cslot 17218  ndxcnx 17230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-res 5697  df-iota 6514  df-fun 6563  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-sets 17201  df-slot 17219

This theorem is referenced by:  resseqnbas  17287  resslemOLD  17288  oppchomfval  17757  oppcbas  17761  rescbas  17873  rescco  17876  rescabs  17877  rescabsOLD  17878  odubas  18336  odubasOLD  18337  setsplusg  19368  oppglemOLD  19369  opprlem  20339  opprlemOLD  20340  rmodislmod  20928  sralem  21175  sralemOLD  21176  srasca  21183  srascaOLD  21184  sravsca  21185  sravscaOLD  21186  zlmlem  21527  zlmlemOLD  21528  zlmsca  21535  znbaslem  21553  znbaslemOLD  21554  thlbas  21714  thlbasOLD  21715  thlle  21716  thlleOLD  21717  opsrbaslem  22067  opsrbaslemOLD  22068  matbas  22417  matplusg  22418  matsca  22419  matscaOLD  22420  matvsca  22421  matvscaOLD  22422  tuslem  24275  tuslemOLD  24276  setsmsbas  24485  setsmsbasOLD  24486  setsmsds  24487  setsmsdsOLD  24488  tnglem  24653  tnglemOLD  24654  tngds  24668  tngdsOLD  24669  ttgval  28883  ttgvalOLD  28884  ttglem  28885  ttglemOLD  28886  cchhllem  28901  cchhllemOLD  28902  setsvtx  29052  resvlem  33357  resvlemOLD  33358  zlmds  33961  zlmdsOLD  33962  zlmtset  33963  zlmtsetOLD  33964  hlhilslem  41940  hlhilslemOLD  41941  mnringnmulrd  44228  mnringnmulrdOLD  44229  cznrnglem  48175  cznabel  48176  cznrng  48177  prstcnidlem  49154  prstcnid  49155