Theorem dfatafv2rnb

Description: The alternate function value at a class A is defined, i.e. in the range of the function, iff the function is defined at A . (Contributed by AV, 2-Sep-2022)

	Ref	Expression
Assertion	dfatafv2rnb	|- ( F defAt A <-> ( F '''' A ) e. ran F )

Proof

Step	Hyp	Ref	Expression
1		funressndmafv2rn	|- ( F defAt A -> ( F '''' A ) e. ran F )
2		ndfatafv2nrn	|- ( -. F defAt A -> ( F '''' A ) e/ ran F )
3		df-nel	|- ( ( F '''' A ) e/ ran F <-> -. ( F '''' A ) e. ran F )
4	2 3	sylib	|- ( -. F defAt A -> -. ( F '''' A ) e. ran F )
5	4	con4i	|- ( ( F '''' A ) e. ran F -> F defAt A )
6	1 5	impbii	|- ( F defAt A <-> ( F '''' A ) e. ran F )