This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fnelnfp

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

Ref Expression
Assertion fnelnfp ⊢ F Fn A ∧ X ∈ A → X ∈ dom ⁡ F ∖ I ↔ F ⁡ X ≠ X

Proof

Step Hyp Ref Expression
1 fndifnfp ⊢ F Fn A → dom ⁡ F ∖ I = x ∈ A | F ⁡ x ≠ x
2 1 eleq2d ⊢ F Fn A → X ∈ dom ⁡ F ∖ I ↔ X ∈ x ∈ A | F ⁡ x ≠ x
3 fveq2 ⊢ x = X → F ⁡ x = F ⁡ X
4 id ⊢ x = X → x = X
5 3 4 neeq12d ⊢ x = X → F ⁡ x ≠ x ↔ F ⁡ X ≠ X
6 5 elrab3 ⊢ X ∈ A → X ∈ x ∈ A | F ⁡ x ≠ x ↔ F ⁡ X ≠ X
7 2 6 sylan9bb ⊢ F Fn A ∧ X ∈ A → X ∈ dom ⁡ F ∖ I ↔ F ⁡ X ≠ X