Metamath Proof Explorer

Theorem afv2elrn

Description: An alternate function value belongs to the range of the function, analogous to fvelrn . (Contributed by AV, 3-Sep-2022)

Ref Expression
Assertion afv2elrn 
|- ( ( Fun F /\ A e. dom F ) -> ( F '''' A ) e. ran F )

Proof

Step Hyp Ref Expression
1 fundmdfat 
 |-  ( ( Fun F /\ A e. dom F ) -> F defAt A )
2 dfatafv2rnb 
 |-  ( F defAt A <-> ( F '''' A ) e. ran F )
3 1 2 sylib 
 |-  ( ( Fun F /\ A e. dom F ) -> ( F '''' A ) e. ran F )