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 F A dom F F defAt A

Proof

Step Hyp Ref Expression
1 funres Fun F Fun F A
2 1 anim1ci Fun F A dom F A dom F Fun F A
3 df-dfat F defAt A A dom F Fun F A
4 2 3 sylibr Fun F A dom F F defAt A