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 A F '''' C B

Proof

Step Hyp Ref Expression
1 ffn F : A B F Fn A
2 fnafv2elrn F Fn A C A F '''' C ran F
3 1 2 sylan F : A B C A F '''' C ran F
4 frn F : A B ran F B
5 4 sseld F : A B F '''' C ran F F '''' C B
6 5 adantr F : A B C A F '''' C ran F F '''' C B
7 3 6 mpd F : A B C A F '''' C B