Metamath Proof Explorer


Theorem fundmdfat

Description: A function is defined at any element of its domain. (Contributed by AV, 2-Sep-2022)

Ref Expression
Assertion fundmdfat ( ( Fun 𝐹𝐴 ∈ dom 𝐹 ) → 𝐹 defAt 𝐴 )

Proof

Step Hyp Ref Expression
1 funres ( Fun 𝐹 → Fun ( 𝐹 ↾ { 𝐴 } ) )
2 1 anim1ci ( ( Fun 𝐹𝐴 ∈ dom 𝐹 ) → ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) )
3 df-dfat ( 𝐹 defAt 𝐴 ↔ ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) )
4 2 3 sylibr ( ( Fun 𝐹𝐴 ∈ dom 𝐹 ) → 𝐹 defAt 𝐴 )