Theorem fnelnfp

Description: Property of a non-fixed point of a function. (Contributed by Stefan O'Rear, 15-Aug-2015)

	Ref	Expression
Assertion	fnelnfp	$$⊢\left(FFnA\wedge X\in A\right)\to \left(X\in \mathrm{dom}\left(F\setminus \mathrm{I}\right)\leftrightarrow F\left(X\right)\ne X\right)$$

Proof

Step	Hyp	Ref	Expression
1		fndifnfp	$$⊢FFnA\to \mathrm{dom}\left(F\setminus \mathrm{I}\right)=\left\{x\in A|F\left(x\right)\ne x\right\}$$
2	1	eleq2d	$$⊢FFnA\to \left(X\in \mathrm{dom}\left(F\setminus \mathrm{I}\right)\leftrightarrow X\in \left\{x\in A|F\left(x\right)\ne x\right\}\right)$$
3		fveq2	$$⊢x=X\to F\left(x\right)=F\left(X\right)$$
4		id	$$⊢x=X\to x=X$$
5	3 4	neeq12d	$$⊢x=X\to \left(F\left(x\right)\ne x\leftrightarrow F\left(X\right)\ne X\right)$$
6	5	elrab3	$$⊢X\in A\to \left(X\in \left\{x\in A|F\left(x\right)\ne x\right\}\leftrightarrow F\left(X\right)\ne X\right)$$
7	2 6	sylan9bb	$$⊢\left(FFnA\wedge X\in A\right)\to \left(X\in \mathrm{dom}\left(F\setminus \mathrm{I}\right)\leftrightarrow F\left(X\right)\ne X\right)$$