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

Metamath Proof Explorer

Theorem dff14b

Description: A one-to-one function in terms of different function values for different arguments. (Contributed by Alexander van der Vekens, 26-Jan-2018)

Ref Expression
Assertion dff14b 
|- ( F : A -1-1-> B <-> ( F : A --> B /\ A. x e. A A. y e. ( A \ { x } ) ( F ` x ) =/= ( F ` y ) ) )

Proof

Step Hyp Ref Expression
1 dff14a 
 |-  ( F : A -1-1-> B <-> ( F : A --> B /\ A. x e. A A. y e. A ( x =/= y -> ( F ` x ) =/= ( F ` y ) ) ) )
2 necom 
 |-  ( x =/= y <-> y =/= x )
3 2 imbi1i 
 |-  ( ( x =/= y -> ( F ` x ) =/= ( F ` y ) ) <-> ( y =/= x -> ( F ` x ) =/= ( F ` y ) ) )
4 3 ralbii 
 |-  ( A. y e. A ( x =/= y -> ( F ` x ) =/= ( F ` y ) ) <-> A. y e. A ( y =/= x -> ( F ` x ) =/= ( F ` y ) ) )
5 raldifsnb 
 |-  ( A. y e. A ( y =/= x -> ( F ` x ) =/= ( F ` y ) ) <-> A. y e. ( A \ { x } ) ( F ` x ) =/= ( F ` y ) )
6 4 5 bitri 
 |-  ( A. y e. A ( x =/= y -> ( F ` x ) =/= ( F ` y ) ) <-> A. y e. ( A \ { x } ) ( F ` x ) =/= ( F ` y ) )
7 6 ralbii 
 |-  ( A. x e. A A. y e. A ( x =/= y -> ( F ` x ) =/= ( F ` y ) ) <-> A. x e. A A. y e. ( A \ { x } ) ( F ` x ) =/= ( F ` y ) )
8 7 anbi2i 
 |-  ( ( F : A --> B /\ A. x e. A A. y e. A ( x =/= y -> ( F ` x ) =/= ( F ` y ) ) ) <-> ( F : A --> B /\ A. x e. A A. y e. ( A \ { x } ) ( F ` x ) =/= ( F ` y ) ) )
9 1 8 bitri 
 |-  ( F : A -1-1-> B <-> ( F : A --> B /\ A. x e. A A. y e. ( A \ { x } ) ( F ` x ) =/= ( F ` y ) ) )