Theorem fvn0fvelrn

Description: If the value of a function is not null, the value is an element of the range of the function. (Contributed by Alexander van der Vekens, 22-Jul-2018) (Proof shortened by SN, 13-Jan-2025)

	Ref	Expression
Assertion	fvn0fvelrn	$$⊢F\left(X\right)\ne \varnothing \to F\left(X\right)\in \mathrm{ran}F$$

Proof

Step	Hyp	Ref	Expression
1		fvrn0	$$⊢F\left(X\right)\in \left(\mathrm{ran}F\cup \left\{\varnothing \right\}\right)$$
2		nelsn	$$⊢F\left(X\right)\ne \varnothing \to \neg F\left(X\right)\in \left\{\varnothing \right\}$$
3		elunnel2	$$⊢\left(F\left(X\right)\in \left(\mathrm{ran}F\cup \left\{\varnothing \right\}\right)\wedge \neg F\left(X\right)\in \left\{\varnothing \right\}\right)\to F\left(X\right)\in \mathrm{ran}F$$
4	1 2 3	sylancr	$$⊢F\left(X\right)\ne \varnothing \to F\left(X\right)\in \mathrm{ran}F$$