Theorem preimafvn0

Description: The preimage of a function value is not empty. (Contributed by AV, 7-Mar-2024)

	Ref	Expression
Assertion	preimafvn0	$$⊢\left(FFnA\wedge X\in A\right)\to F^{-1}\left[\left\{F\left(X\right)\right\}\right]\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		preimafvsnel	$$⊢\left(FFnA\wedge X\in A\right)\to X\in F^{-1}\left[\left\{F\left(X\right)\right\}\right]$$
2	1	ne0d	$$⊢\left(FFnA\wedge X\in A\right)\to F^{-1}\left[\left\{F\left(X\right)\right\}\right]\ne \varnothing$$