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	imbitrid	|- ( 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 ) )