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

Metamath Proof Explorer

Theorem dff14a

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 dff14a 
|- ( F : A -1-1-> B <-> ( F : A --> B /\ A. x e. A A. y e. A ( x =/= y -> ( F ` x ) =/= ( F ` y ) ) ) )

Proof

Step Hyp Ref Expression
1 dff13 
 |-  ( F : A -1-1-> B <-> ( F : A --> B /\ A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
2 con34b 
 |-  ( ( ( F ` x ) = ( F ` y ) -> x = y ) <-> ( -. x = y -> -. ( F ` x ) = ( F ` y ) ) )
3 df-ne 
 |-  ( x =/= y <-> -. x = y )
4 3 bicomi 
 |-  ( -. x = y <-> x =/= y )
5 df-ne 
 |-  ( ( F ` x ) =/= ( F ` y ) <-> -. ( F ` x ) = ( F ` y ) )
6 5 bicomi 
 |-  ( -. ( F ` x ) = ( F ` y ) <-> ( F ` x ) =/= ( F ` y ) )
7 4 6 imbi12i 
 |-  ( ( -. x = y -> -. ( F ` x ) = ( F ` y ) ) <-> ( x =/= y -> ( F ` x ) =/= ( F ` y ) ) )
8 2 7 bitri 
 |-  ( ( ( F ` x ) = ( F ` y ) -> x = y ) <-> ( x =/= y -> ( F ` x ) =/= ( F ` y ) ) )
9 8 2ralbii 
 |-  ( A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) <-> A. x e. A A. y e. A ( x =/= y -> ( F ` x ) =/= ( F ` y ) ) )
10 9 anbi2i 
 |-  ( ( F : A --> B /\ A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) ) <-> ( F : A --> B /\ A. x e. A A. y e. A ( x =/= y -> ( F ` x ) =/= ( F ` y ) ) ) )
11 1 10 bitri 
 |-  ( F : A -1-1-> B <-> ( F : A --> B /\ A. x e. A A. y e. A ( x =/= y -> ( F ` x ) =/= ( F ` y ) ) ) )