Metamath Proof Explorer

Theorem fnafvelrn

Description: A function's value belongs to its range, analogous to fnfvelrn . (Contributed by Alexander van der Vekens, 25-May-2017)

Ref Expression
Assertion fnafvelrn 
|- ( ( F Fn A /\ B e. A ) -> ( F ''' B ) e. ran F )

Proof

Step Hyp Ref Expression
1 afvelrn 
 |-  ( ( Fun F /\ B e. dom F ) -> ( F ''' B ) e. ran F )
2 1 funfni 
 |-  ( ( F Fn A /\ B e. A ) -> ( F ''' B ) e. ran F )