Metamath Proof Explorer


Theorem frnvafv2v

Description: If the codomain of a function is a set, the alternate function value is always also a set. (Contributed by AV, 4-Sep-2022)

Ref Expression
Assertion frnvafv2v
|- ( ( F : A --> B /\ B e. V ) -> ( F '''' C ) e. _V )

Proof

Step Hyp Ref Expression
1 df-f
 |-  ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
2 ssexg
 |-  ( ( ran F C_ B /\ B e. V ) -> ran F e. _V )
3 2 ex
 |-  ( ran F C_ B -> ( B e. V -> ran F e. _V ) )
4 1 3 simplbiim
 |-  ( F : A --> B -> ( B e. V -> ran F e. _V ) )
5 4 imp
 |-  ( ( F : A --> B /\ B e. V ) -> ran F e. _V )
6 afv2ex
 |-  ( ran F e. _V -> ( F '''' C ) e. _V )
7 5 6 syl
 |-  ( ( F : A --> B /\ B e. V ) -> ( F '''' C ) e. _V )