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 e. A ) -> ( X e. dom ( F \ _I ) <-> ( F ` X ) =/= X ) )

Proof

Step Hyp Ref Expression
1 fndifnfp 
 |-  ( F Fn A -> dom ( F \ _I ) = { x e. A | ( F ` x ) =/= x } )
2 1 eleq2d 
 |-  ( F Fn A -> ( X e. dom ( F \ _I ) <-> X e. { x e. 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 e. A -> ( X e. { x e. A | ( F ` x ) =/= x } <-> ( F ` X ) =/= X ) )
7 2 6 sylan9bb 
 |-  ( ( F Fn A /\ X e. A ) -> ( X e. dom ( F \ _I ) <-> ( F ` X ) =/= X ) )