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 e. A <-> ( F '''' C ) e. ran F ) )

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