Metamath Proof Explorer


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 )