Metamath Proof Explorer

Theorem dff15

Description: A one-to-one function in terms of different arguments never having the same function value. (Contributed by BTernaryTau, 24-Oct-2023)

Ref Expression
Assertion dff15 
|- ( F : A -1-1-> B <-> ( F : A --> B /\ -. E. x e. A E. y e. A ( ( F ` x ) = ( F ` y ) /\ x =/= 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 iman 
 |-  ( ( ( F ` x ) = ( F ` y ) -> x = y ) <-> -. ( ( F ` x ) = ( F ` y ) /\ -. x = y ) )
3 df-ne 
 |-  ( x =/= y <-> -. x = y )
4 3 anbi2i 
 |-  ( ( ( F ` x ) = ( F ` y ) /\ x =/= y ) <-> ( ( F ` x ) = ( F ` y ) /\ -. x = y ) )
5 2 4 xchbinxr 
 |-  ( ( ( F ` x ) = ( F ` y ) -> x = y ) <-> -. ( ( F ` x ) = ( F ` y ) /\ x =/= y ) )
6 5 2ralbii 
 |-  ( A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) <-> A. x e. A A. y e. A -. ( ( F ` x ) = ( F ` y ) /\ x =/= y ) )
7 ralnex2 
 |-  ( A. x e. A A. y e. A -. ( ( F ` x ) = ( F ` y ) /\ x =/= y ) <-> -. E. x e. A E. y e. A ( ( F ` x ) = ( F ` y ) /\ x =/= y ) )
8 6 7 bitri 
 |-  ( A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) <-> -. E. x e. A E. y e. A ( ( F ` x ) = ( F ` y ) /\ x =/= y ) )
9 8 anbi2i 
 |-  ( ( F : A --> B /\ A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) ) <-> ( F : A --> B /\ -. E. x e. A E. y e. A ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) )
10 1 9 bitri 
 |-  ( F : A -1-1-> B <-> ( F : A --> B /\ -. E. x e. A E. y e. A ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) )