Metamath Proof Explorer


Theorem fexafv2ex

Description: The alternate function value is always a set if the function (resp. the domain of the function) is a set. (Contributed by AV, 3-Sep-2022)

Ref Expression
Assertion fexafv2ex
|- ( F e. V -> ( F '''' A ) e. _V )

Proof

Step Hyp Ref Expression
1 rnexg
 |-  ( F e. V -> ran F e. _V )
2 afv2ex
 |-  ( ran F e. _V -> ( F '''' A ) e. _V )
3 1 2 syl
 |-  ( F e. V -> ( F '''' A ) e. _V )