# 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 𝐹𝑋 ∈ dom 𝐹 ) → ( ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , ( 𝐹𝑋 ) ⟩ } ) = 𝐹 )

### Proof

Step Hyp Ref Expression
1 funrel ( Fun 𝐹 → Rel 𝐹 )
2 resdmdfsn ( Rel 𝐹 → ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) = ( 𝐹 ↾ ( dom 𝐹 ∖ { 𝑋 } ) ) )
3 1 2 syl ( Fun 𝐹 → ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) = ( 𝐹 ↾ ( dom 𝐹 ∖ { 𝑋 } ) ) )
4 3 adantr ( ( Fun 𝐹𝑋 ∈ dom 𝐹 ) → ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) = ( 𝐹 ↾ ( dom 𝐹 ∖ { 𝑋 } ) ) )
5 4 uneq1d ( ( Fun 𝐹𝑋 ∈ dom 𝐹 ) → ( ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , ( 𝐹𝑋 ) ⟩ } ) = ( ( 𝐹 ↾ ( dom 𝐹 ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , ( 𝐹𝑋 ) ⟩ } ) )
6 funfn ( Fun 𝐹𝐹 Fn dom 𝐹 )
7 fnsnsplit ( ( 𝐹 Fn dom 𝐹𝑋 ∈ dom 𝐹 ) → 𝐹 = ( ( 𝐹 ↾ ( dom 𝐹 ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , ( 𝐹𝑋 ) ⟩ } ) )
8 6 7 sylanb ( ( Fun 𝐹𝑋 ∈ dom 𝐹 ) → 𝐹 = ( ( 𝐹 ↾ ( dom 𝐹 ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , ( 𝐹𝑋 ) ⟩ } ) )
9 5 8 eqtr4d ( ( Fun 𝐹𝑋 ∈ dom 𝐹 ) → ( ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , ( 𝐹𝑋 ) ⟩ } ) = 𝐹 )