Metamath Proof Explorer

Theorem dfatelrn

Description: The value of a function F at a set A is in the range of the function F if F is defined at A . (Contributed by AV, 1-Sep-2022)

Ref Expression
Assertion dfatelrn 
|- ( F defAt A -> ( F ` A ) e. ran F )

Proof

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