Theorem fvfundmfvn0

Description: If the "value of a class" at an argument is not the empty set, then the argument is in the domain of the class and the class restricted to the singleton formed on that argument is a function. (Contributed by Alexander van der Vekens, 26-May-2017) (Proof shortened by BJ, 13-Aug-2022)

	Ref	Expression
Assertion	fvfundmfvn0	|- ( ( F ` A ) =/= (/) -> ( A e. dom F /\ Fun ( F |` { A } ) ) )

Proof

Step	Hyp	Ref	Expression
1		ndmfv	|- ( -. A e. dom F -> ( F ` A ) = (/) )
2	1	necon1ai	|- ( ( F ` A ) =/= (/) -> A e. dom F )
3		nfunsn	|- ( -. Fun ( F |` { A } ) -> ( F ` A ) = (/) )
4	3	necon1ai	|- ( ( F ` A ) =/= (/) -> Fun ( F |` { A } ) )
5	2 4	jca	|- ( ( F ` A ) =/= (/) -> ( A e. dom F /\ Fun ( F |` { A } ) ) )