Theorem preimafvsnel

Description: The preimage of a function value at X contains X . (Contributed by AV, 7-Mar-2024)

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

Proof

Step	Hyp	Ref	Expression
1		simpr	$$⊢\left(FFnA\wedge X\in A\right)\to X\in A$$
2		eqidd	$$⊢\left(FFnA\wedge X\in A\right)\to F\left(X\right)=F\left(X\right)$$
3		fniniseg	$$⊢FFnA\to \left(X\in F^{-1}\left[\left\{F\left(X\right)\right\}\right]\leftrightarrow \left(X\in A\wedge F\left(X\right)=F\left(X\right)\right)\right)$$
4	3	adantr	$$⊢\left(FFnA\wedge X\in A\right)\to \left(X\in F^{-1}\left[\left\{F\left(X\right)\right\}\right]\leftrightarrow \left(X\in A\wedge F\left(X\right)=F\left(X\right)\right)\right)$$
5	1 2 4	mpbir2and	$$⊢\left(FFnA\wedge X\in A\right)\to X\in F^{-1}\left[\left\{F\left(X\right)\right\}\right]$$