Theorem fnelnfp

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

	Ref	Expression
Assertion	fnelnfp	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑋 ∈ dom ( 𝐹 ∖ I ) ↔ ( 𝐹 ‘ 𝑋 ) ≠ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		fndifnfp	⊢ ( 𝐹 Fn 𝐴 → dom ( 𝐹 ∖ I ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 𝑥 } )
2	1	eleq2d	⊢ ( 𝐹 Fn 𝐴 → ( 𝑋 ∈ dom ( 𝐹 ∖ I ) ↔ 𝑋 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 𝑥 } ) )
3		fveq2	⊢ ( 𝑥 = 𝑋 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
4		id	⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
5	3 4	neeq12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ 𝑥 ) ≠ 𝑥 ↔ ( 𝐹 ‘ 𝑋 ) ≠ 𝑋 ) )
6	5	elrab3	⊢ ( 𝑋 ∈ 𝐴 → ( 𝑋 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 𝑥 } ↔ ( 𝐹 ‘ 𝑋 ) ≠ 𝑋 ) )
7	2 6	sylan9bb	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑋 ∈ dom ( 𝐹 ∖ I ) ↔ ( 𝐹 ‘ 𝑋 ) ≠ 𝑋 ) )