Theorem afv2res 48582

Description: The value of a restricted function for an argument at which the function is defined. Analog to fvres 6935. (Contributed by AV, 5-Sep-2022.)

Assertion

Ref	Expression
afv2res	⊢ ((𝐹 defAt 𝐴 ∧ 𝐴 ∈ 𝐵) → ((𝐹 ↾ 𝐵)''''𝐴) = (𝐹''''𝐴))

Proof of Theorem afv2res

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-dfat 48463	. . . . 5 ⊢ (𝐹 defAt 𝐴 ↔ (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})))
2		elin 4096	. . . . . . . . . 10 ⊢ (𝐴 ∈ (𝐵 ∩ dom 𝐹) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ dom 𝐹))
3	2	biimpri 231	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ dom 𝐹) → 𝐴 ∈ (𝐵 ∩ dom 𝐹))
4		dmres 6020	. . . . . . . . 9 ⊢ dom (𝐹 ↾ 𝐵) = (𝐵 ∩ dom 𝐹)
5	3, 4	eleqtrrdi 2875	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ dom 𝐹) → 𝐴 ∈ dom (𝐹 ↾ 𝐵))
6	5	ex 418	. . . . . . 7 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ dom 𝐹 → 𝐴 ∈ dom (𝐹 ↾ 𝐵)))
7		snssi 4748	. . . . . . . . . . 11 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)
8	7	resabs1d 6016	. . . . . . . . . 10 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵) ↾ {𝐴}) = (𝐹 ↾ {𝐴}))
9	8	eqcomd 2769	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝐵 → (𝐹 ↾ {𝐴}) = ((𝐹 ↾ 𝐵) ↾ {𝐴}))
10	9	funeqd 6589	. . . . . . . 8 ⊢ (𝐴 ∈ 𝐵 → (Fun (𝐹 ↾ {𝐴}) ↔ Fun ((𝐹 ↾ 𝐵) ↾ {𝐴})))
11	10	biimpd 232	. . . . . . 7 ⊢ (𝐴 ∈ 𝐵 → (Fun (𝐹 ↾ {𝐴}) → Fun ((𝐹 ↾ 𝐵) ↾ {𝐴})))
12	6, 11	anim12d 621	. . . . . 6 ⊢ (𝐴 ∈ 𝐵 → ((𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})) → (𝐴 ∈ dom (𝐹 ↾ 𝐵) ∧ Fun ((𝐹 ↾ 𝐵) ↾ {𝐴}))))
13	12	com12 33	. . . . 5 ⊢ ((𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})) → (𝐴 ∈ 𝐵 → (𝐴 ∈ dom (𝐹 ↾ 𝐵) ∧ Fun ((𝐹 ↾ 𝐵) ↾ {𝐴}))))
14	1, 13	sylbi 220	. . . 4 ⊢ (𝐹 defAt 𝐴 → (𝐴 ∈ 𝐵 → (𝐴 ∈ dom (𝐹 ↾ 𝐵) ∧ Fun ((𝐹 ↾ 𝐵) ↾ {𝐴}))))
15	14	imp 412	. . 3 ⊢ ((𝐹 defAt 𝐴 ∧ 𝐴 ∈ 𝐵) → (𝐴 ∈ dom (𝐹 ↾ 𝐵) ∧ Fun ((𝐹 ↾ 𝐵) ↾ {𝐴})))
16		df-dfat 48463	. . . 4 ⊢ ((𝐹 ↾ 𝐵) defAt 𝐴 ↔ (𝐴 ∈ dom (𝐹 ↾ 𝐵) ∧ Fun ((𝐹 ↾ 𝐵) ↾ {𝐴})))
17		dfatafv2iota 48553	. . . 4 ⊢ ((𝐹 ↾ 𝐵) defAt 𝐴 → ((𝐹 ↾ 𝐵)''''𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥))
18	16, 17	sylbir 238	. . 3 ⊢ ((𝐴 ∈ dom (𝐹 ↾ 𝐵) ∧ Fun ((𝐹 ↾ 𝐵) ↾ {𝐴})) → ((𝐹 ↾ 𝐵)''''𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥))
19	15, 18	syl 18	. 2 ⊢ ((𝐹 defAt 𝐴 ∧ 𝐴 ∈ 𝐵) → ((𝐹 ↾ 𝐵)''''𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥))
20		vex 3458	. . . . . 6 ⊢ 𝑥 ∈ V
21	20	brresi 5995	. . . . 5 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴𝐹𝑥))
22	21	baib 545	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
23	22	iotabidv 6549	. . 3 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
24	23	adantl 487	. 2 ⊢ ((𝐹 defAt 𝐴 ∧ 𝐴 ∈ 𝐵) → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
25		dfatafv2iota 48553	. . . 4 ⊢ (𝐹 defAt 𝐴 → (𝐹''''𝐴) = (℩𝑥𝐴𝐹𝑥))
26	25	eqcomd 2769	. . 3 ⊢ (𝐹 defAt 𝐴 → (℩𝑥𝐴𝐹𝑥) = (𝐹''''𝐴))
27	26	adantr 486	. 2 ⊢ ((𝐹 defAt 𝐴 ∧ 𝐴 ∈ 𝐵) → (℩𝑥𝐴𝐹𝑥) = (𝐹''''𝐴))
28	19, 24, 27	3eqtrd 2802	1 ⊢ ((𝐹 defAt 𝐴 ∧ 𝐴 ∈ 𝐵) → ((𝐹 ↾ 𝐵)''''𝐴) = (𝐹''''𝐴))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147   ∩ cin 4092  {csn 4588   class class class wbr 5108  dom cdm 5658   ↾ cres 5660  ℩cio 6518  Fun wfun 6560   defAt wdfat 48460  ''''cafv2 48551

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-res 5670  df-iota 6520  df-fun 6568  df-dfat 48463  df-afv2 48552

This theorem is used by: (None)