Theorem setsnid 17256

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 23	. . . 4 ⊢ (𝑊 ∈ V → 𝑊 ∈ V)
3	1, 2	strfvnd 17233	. . 3 ⊢ (𝑊 ∈ V → (𝐸‘𝑊) = (𝑊‘(𝐸‘ndx)))
4		ovex 7433	. . . . 5 ⊢ (𝑊 sSet ⟨𝐷, 𝐶⟩) ∈ V
5	4, 1	strfvn 17234	. . . 4 ⊢ (𝐸‘(𝑊 sSet ⟨𝐷, 𝐶⟩)) = ((𝑊 sSet ⟨𝐷, 𝐶⟩)‘(𝐸‘ndx))
6		setsres 17226	. . . . . 6 ⊢ (𝑊 ∈ V → ((𝑊 sSet ⟨𝐷, 𝐶⟩) ↾ (V ∖ {𝐷})) = (𝑊 ↾ (V ∖ {𝐷})))
7	6	fveq1d 6873	. . . . 5 ⊢ (𝑊 ∈ V → (((𝑊 sSet ⟨𝐷, 𝐶⟩) ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = ((𝑊 ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)))
8		fvex 6884	. . . . . . 7 ⊢ (𝐸‘ndx) ∈ V
9		setsnid.n	. . . . . . 7 ⊢ (𝐸‘ndx) ≠ 𝐷
10		eldifsn 4749	. . . . . . 7 ⊢ ((𝐸‘ndx) ∈ (V ∖ {𝐷}) ↔ ((𝐸‘ndx) ∈ V ∧ (𝐸‘ndx) ≠ 𝐷))
11	8, 9, 10	mpbir2an 723	. . . . . 6 ⊢ (𝐸‘ndx) ∈ (V ∖ {𝐷})
12		fvres 6890	. . . . . 6 ⊢ ((𝐸‘ndx) ∈ (V ∖ {𝐷}) → (((𝑊 sSet ⟨𝐷, 𝐶⟩) ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = ((𝑊 sSet ⟨𝐷, 𝐶⟩)‘(𝐸‘ndx)))
13	11, 12	ax-mp 5	. . . . 5 ⊢ (((𝑊 sSet ⟨𝐷, 𝐶⟩) ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = ((𝑊 sSet ⟨𝐷, 𝐶⟩)‘(𝐸‘ndx))
14		fvres 6890	. . . . . 6 ⊢ ((𝐸‘ndx) ∈ (V ∖ {𝐷}) → ((𝑊 ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = (𝑊‘(𝐸‘ndx)))
15	11, 14	ax-mp 5	. . . . 5 ⊢ ((𝑊 ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = (𝑊‘(𝐸‘ndx))
16	7, 13, 15	3eqtr3g 2823	. . . 4 ⊢ (𝑊 ∈ V → ((𝑊 sSet ⟨𝐷, 𝐶⟩)‘(𝐸‘ndx)) = (𝑊‘(𝐸‘ndx)))
17	5, 16	eqtrid 2812	. . 3 ⊢ (𝑊 ∈ V → (𝐸‘(𝑊 sSet ⟨𝐷, 𝐶⟩)) = (𝑊‘(𝐸‘ndx)))
18	3, 17	eqtr4d 2803	. 2 ⊢ (𝑊 ∈ V → (𝐸‘𝑊) = (𝐸‘(𝑊 sSet ⟨𝐷, 𝐶⟩)))
19	1	str0 17237	. . . 4 ⊢ ∅ = (𝐸‘∅)
20	19	eqcomi 2774	. . 3 ⊢ (𝐸‘∅) = ∅
21		eqid 2765	. . 3 ⊢ (𝑊 sSet ⟨𝐷, 𝐶⟩) = (𝑊 sSet ⟨𝐷, 𝐶⟩)
22		reldmsets 17213	. . 3 ⊢ Rel dom sSet
23	20, 21, 22	oveqprc 17240	. 2 ⊢ (¬ 𝑊 ∈ V → (𝐸‘𝑊) = (𝐸‘(𝑊 sSet ⟨𝐷, 𝐶⟩)))
24	18, 23	pm2.61i 184	1 ⊢ (𝐸‘𝑊) = (𝐸‘(𝑊 sSet ⟨𝐷, 𝐶⟩))

Syntax hints:   = wceq 1563   ∈ wcel 2145   ≠ wne 2960  Vcvv 3457   ∖ cdif 3904  ∅c0 4288  {csn 4585  ⟨cop 4591   ↾ cres 5653  ‘cfv 6525  (class class class)co 7400   sSet csts 17211  Slot cslot 17229  ndxcnx 17241

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-nul 5260  ax-pr 5394  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-sbc 3748  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-res 5663  df-iota 6481  df-fun 6527  df-fv 6533  df-ov 7403  df-oprab 7404  df-mpo 7405  df-sets 17212  df-slot 17230

This theorem is referenced by:  resseqnbas  17290  oppchomfval  17758  oppcbas  17762  rescbas  17874  rescco  17877  rescabs  17878  odubas  18335  setsplusg  19408  opprlem  20412  rmodislmod  21017  sralem  21263  srasca  21267  sravsca  21268  zlmlem  21623  zlmsca  21627  znbaslem  21645  thlbas  21803  thlle  21804  opsrbaslem  22157  matbas  22527  matplusg  22528  matsca  22529  matvsca  22530  tuslem  24380  setsmsbas  24589  setsmsds  24590  tnglem  24754  tngds  24762  ttgval  29129  ttglem  29130  cchhllem  29141  setsvtx  29290  resvlem  33563  zlmds  34264  zlmtset  34265  hlhilslem  42569  mnringnmulrd  44797  cznrnglem  48880  cznabel  48881  cznrng  48882  prstcnidlem  50182  prstcnid  50183