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 V F '''' C V

Proof

Step Hyp Ref Expression
1 df-f F : A B F Fn A ran F B
2 ssexg ran F B B V ran F V
3 2 ex ran F B B V ran F V
4 1 3 simplbiim F : A B B V ran F V
5 4 imp F : A B B V ran F V
6 afv2ex ran F V F '''' C V
7 5 6 syl F : A B B V F '''' C V