Metamath Proof Explorer


Theorem fafv2elrnb

Description: An alternate function value is defined, i.e., belongs to the range of the function, iff its argument is in the domain of the function. (Contributed by AV, 3-Sep-2022)

Ref Expression
Assertion fafv2elrnb F : A B C A F '''' C ran F

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 3 ex F : A B C A F '''' C ran F
5 fdm F : A B dom F = A
6 ndmafv2nrn ¬ C dom F F '''' C ran F
7 df-nel F '''' C ran F ¬ F '''' C ran F
8 6 7 sylib ¬ C dom F ¬ F '''' C ran F
9 8 con4i F '''' C ran F C dom F
10 eleq2 dom F = A C dom F C A
11 9 10 syl5ib dom F = A F '''' C ran F C A
12 5 11 syl F : A B F '''' C ran F C A
13 4 12 impbid F : A B C A F '''' C ran F