This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem funresdfunsn

Description: Restricting a function to a domain without one element of the domain of the function, and adding a pair of this element and the function value of the element results in the function itself. (Contributed by AV, 2-Dec-2018)

Ref Expression
Assertion funresdfunsn ⊢ Fun ⁡ F ∧ X ∈ dom ⁡ F → F ↾ V ∖ X ∪ X F ⁡ X = F

Proof

Step Hyp Ref Expression
1 funrel ⊢ Fun ⁡ F → Rel ⁡ F
2 resdmdfsn ⊢ Rel ⁡ F → F ↾ V ∖ X = F ↾ dom ⁡ F ∖ X
3 1 2 syl ⊢ Fun ⁡ F → F ↾ V ∖ X = F ↾ dom ⁡ F ∖ X
4 3 adantr ⊢ Fun ⁡ F ∧ X ∈ dom ⁡ F → F ↾ V ∖ X = F ↾ dom ⁡ F ∖ X
5 4 uneq1d ⊢ Fun ⁡ F ∧ X ∈ dom ⁡ F → F ↾ V ∖ X ∪ X F ⁡ X = F ↾ dom ⁡ F ∖ X ∪ X F ⁡ X
6 funfn ⊢ Fun ⁡ F ↔ F Fn dom ⁡ F
7 fnsnsplit ⊢ F Fn dom ⁡ F ∧ X ∈ dom ⁡ F → F = F ↾ dom ⁡ F ∖ X ∪ X F ⁡ X
8 6 7 sylanb ⊢ Fun ⁡ F ∧ X ∈ dom ⁡ F → F = F ↾ dom ⁡ F ∖ X ∪ X F ⁡ X
9 5 8 eqtr4d ⊢ Fun ⁡ F ∧ X ∈ dom ⁡ F → F ↾ V ∖ X ∪ X F ⁡ X = F