Theorem fcdmvafv2v

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	fcdmvafv2v	|- ( ( 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 )