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

Proof

Step Hyp Ref Expression
1 funres 
 |-  ( Fun F -> Fun ( F |` { A } ) )
2 1 anim1ci 
 |-  ( ( Fun F /\ A e. dom F ) -> ( A e. dom F /\ Fun ( F |` { A } ) ) )
3 df-dfat 
 |-  ( F defAt A <-> ( A e. dom F /\ Fun ( F |` { A } ) ) )
4 2 3 sylibr 
 |-  ( ( Fun F /\ A e. dom F ) -> F defAt A )