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\left(A\right)\ne \varnothing \to \left(A\in \mathrm{dom}F\wedge \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ndmfv	$$⊢\neg A\in \mathrm{dom}F\to F\left(A\right)=\varnothing$$
2	1	necon1ai	$$⊢F\left(A\right)\ne \varnothing \to A\in \mathrm{dom}F$$
3		nfunsn	$$⊢\neg \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to F\left(A\right)=\varnothing$$
4	3	necon1ai	$$⊢F\left(A\right)\ne \varnothing \to \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)$$
5	2 4	jca	$$⊢F\left(A\right)\ne \varnothing \to \left(A\in \mathrm{dom}F\wedge \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\right)$$