Theorem fnelfp

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

	Ref	Expression
Assertion	fnelfp	$$⊢\left(FFnA\wedge X\in A\right)\to \left(X\in \mathrm{dom}\left(F\cap \mathrm{I}\right)\leftrightarrow F\left(X\right)=X\right)$$

Proof

Step	Hyp	Ref	Expression
1		fninfp	$$⊢FFnA\to \mathrm{dom}\left(F\cap \mathrm{I}\right)=\left\{x\in A|F\left(x\right)=x\right\}$$
2	1	eleq2d	$$⊢FFnA\to \left(X\in \mathrm{dom}\left(F\cap \mathrm{I}\right)\leftrightarrow X\in \left\{x\in A|F\left(x\right)=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	eqeq12d	$$⊢x=X\to \left(F\left(x\right)=x\leftrightarrow F\left(X\right)=X\right)$$
6	5	elrab3	$$⊢X\in A\to \left(X\in \left\{x\in A|F\left(x\right)=x\right\}\leftrightarrow F\left(X\right)=X\right)$$
7	2 6	sylan9bb	$$⊢\left(FFnA\wedge X\in A\right)\to \left(X\in \mathrm{dom}\left(F\cap \mathrm{I}\right)\leftrightarrow F\left(X\right)=X\right)$$