fnelfp

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

		Ref	Expression
	Assertion	fnelfp	$⊢ (F Fn A \land X \in A) \to (X \in dom (F \cap I) \leftrightarrow F (X) = X)$

Step	Hyp	Ref	Expression
1		fninfp	$⊢ F Fn A \to dom (F \cap I) = \{x \in A \| F (x) = x\}$
2	1	eleq2d	$⊢ F Fn A \to (X \in dom (F \cap I) \leftrightarrow X \in \{x \in A \| F (x) = x\})$
3		fveq2	$⊢ x = X \to F (x) = F (X)$
4		id	$⊢ x = X \to x = X$
5	3 4	eqeq12d	$⊢ x = X \to (F (x) = x \leftrightarrow F (X) = X)$
6	5	elrab3	$⊢ X \in A \to (X \in \{x \in A \| F (x) = x\} \leftrightarrow F (X) = X)$
7	2 6	sylan9bb	$⊢ (F Fn A \land X \in A) \to (X \in dom (F \cap I) \leftrightarrow F (X) = X)$

Metamath Proof Explorer