Theorem fafv2elrn

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

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

Proof

Step	Hyp	Ref	Expression
1		ffn	|- ( F : A --> B -> F Fn A )
2		fnafv2elrn	|- ( ( F Fn A /\ C e. A ) -> ( F '''' C ) e. ran F )
3	1 2	sylan	|- ( ( F : A --> B /\ C e. A ) -> ( F '''' C ) e. ran F )
4		frn	|- ( F : A --> B -> ran F C_ B )
5	4	sseld	|- ( F : A --> B -> ( ( F '''' C ) e. ran F -> ( F '''' C ) e. B ) )
6	5	adantr	|- ( ( F : A --> B /\ C e. A ) -> ( ( F '''' C ) e. ran F -> ( F '''' C ) e. B ) )
7	3 6	mpd	|- ( ( F : A --> B /\ C e. A ) -> ( F '''' C ) e. B )