Metamath Proof Explorer

Theorem afv2res

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

Ref Expression
Assertion afv2res ⊢ F defAt A ∧ A ∈ B → F ↾ B '''' A = F '''' A

Proof

Step Hyp Ref Expression
1 df-dfat ⊢ F defAt A ↔ A ∈ dom ⁡ F ∧ Fun ⁡ F ↾ A
2 elin ⊢ A ∈ B ∩ dom ⁡ F ↔ A ∈ B ∧ A ∈ dom ⁡ F
3 2 biimpri ⊢ A ∈ B ∧ A ∈ dom ⁡ F → A ∈ B ∩ dom ⁡ F
4 dmres ⊢ dom ⁡ F ↾ B = B ∩ dom ⁡ F
5 3 4 eleqtrrdi ⊢ A ∈ B ∧ A ∈ dom ⁡ F → A ∈ dom ⁡ F ↾ B
6 5 ex ⊢ A ∈ B → A ∈ dom ⁡ F → A ∈ dom ⁡ F ↾ B
7 snssi ⊢ A ∈ B → A ⊆ B
8 7 resabs1d ⊢ A ∈ B → F ↾ B ↾ A = F ↾ A
9 8 eqcomd ⊢ A ∈ B → F ↾ A = F ↾ B ↾ A
10 9 funeqd ⊢ A ∈ B → Fun ⁡ F ↾ A ↔ Fun ⁡ F ↾ B ↾ A
11 10 biimpd ⊢ A ∈ B → Fun ⁡ F ↾ A → Fun ⁡ F ↾ B ↾ A
12 6 11 anim12d ⊢ A ∈ B → A ∈ dom ⁡ F ∧ Fun ⁡ F ↾ A → A ∈ dom ⁡ F ↾ B ∧ Fun ⁡ F ↾ B ↾ A
13 12 com12 ⊢ A ∈ dom ⁡ F ∧ Fun ⁡ F ↾ A → A ∈ B → A ∈ dom ⁡ F ↾ B ∧ Fun ⁡ F ↾ B ↾ A
14 1 13 sylbi ⊢ F defAt A → A ∈ B → A ∈ dom ⁡ F ↾ B ∧ Fun ⁡ F ↾ B ↾ A
15 14 imp ⊢ F defAt A ∧ A ∈ B → A ∈ dom ⁡ F ↾ B ∧ Fun ⁡ F ↾ B ↾ A
16 df-dfat ⊢ F ↾ B defAt A ↔ A ∈ dom ⁡ F ↾ B ∧ Fun ⁡ F ↾ B ↾ A
17 dfatafv2iota ⊢ F ↾ B defAt A → F ↾ B '''' A = ι x | A F ↾ B x
18 16 17 sylbir ⊢ A ∈ dom ⁡ F ↾ B ∧ Fun ⁡ F ↾ B ↾ A → F ↾ B '''' A = ι x | A F ↾ B x
19 15 18 syl ⊢ F defAt A ∧ A ∈ B → F ↾ B '''' A = ι x | A F ↾ B x
20 vex ⊢ x ∈ V
21 20 brresi ⊢ A F ↾ B x ↔ A ∈ B ∧ A F x
22 21 baib ⊢ A ∈ B → A F ↾ B x ↔ A F x
23 22 iotabidv ⊢ A ∈ B → ι x | A F ↾ B x = ι x | A F x
24 23 adantl ⊢ F defAt A ∧ A ∈ B → ι x | A F ↾ B x = ι x | A F x
25 dfatafv2iota ⊢ F defAt A → F '''' A = ι x | A F x
26 25 eqcomd ⊢ F defAt A → ι x | A F x = F '''' A
27 26 adantr ⊢ F defAt A ∧ A ∈ B → ι x | A F x = F '''' A
28 19 24 27 3eqtrd ⊢ F defAt A ∧ A ∈ B → F ↾ B '''' A = F '''' A