Metamath Proof Explorer

Theorem fnafv2elrn

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

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

Proof

Step Hyp Ref Expression
1 afv2elrn 
 |-  ( ( 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 )