Why is the use of an implication arrow correct in the definition of injective functions: $ \forall a\forall b(f(a) = f(b) \to a = b) $? According to an excerpt, from a textbook, about injective functions:

We can express that $f$ is one-to-one using quantifiers as
  $$ \forall a\forall b(f(a) = f(b) \to a = b) $$
  where the universe of discourse is the domain

I am having trouble understanding why the use of an implication arrow is correct for the definition of injective functions?
My counter example to the definition of injective functions:


*

*The proposition $ f(a) \neq f(b) \to a = b $ would hold true to the definition of injective functions above, as $ \mathbf F \to \mathbf T $ holds true for conditional propositions.

*Because $a = b$ this means that the single input $a$ gives out 2 different output values, $f(a)$ and $f(b)$

*And this goes against the notion of one-to-one, as it becomes one-to-two. And it even goes against the definition of a function in general.


Is my line of reasoning correct? If not, where did I go wrong? Please, explain in detail my fault in the counter example.
And isn't the use of a biconditional arrow the true correct way of defining an injective function?
$$ \forall a\forall b(f(a) = f(b) \iff a = b) $$
 A: You are already assuming that $f$ is a function.  That is, if $f$ is a function, then $f$ is said to be injective if $$\forall a\forall b(f(a) = f(b) \to a = b).$$  Since you have assumed $f$ is a function, you already know that $a=b$ implies $f(a)=f(b)$.  (In fact, it is unclear what "$f(a)$" or "$f(b)$" is supposed to mean if $f$ is not a function.)  It is true that $a=b$ and $f(a)\neq f(b)$ would not contradict the statement $$\forall a\forall b(f(a) = f(b) \to a = b),$$ but it would contradict the assumption that $f$ is a function, and so it cannot happen for an injective function under this definition.
Thus you only need to assert one direction of the implication (though it is harmless to also state the other direction).  That is, if $f$ is a function, the statements $$\forall a\forall b(f(a) = f(b) \to a = b)$$ and $$\forall a\forall b(f(a) = f(b) \iff a = b)$$ are equivalent.
A: "The proposition f(a)≠f(b)→a=b would hold true to the definition above, as F→T
holds true for conditional propositions."
$f(a) \ne f(b)$ isn't a false statement. 
The definition $f(a) \ne f(b) \implies a = b$ would describe constant functions and only constant functions.  
This could be a working definition of "constant function" although it would be convoluted, confusing, and, to anyone who doesn't live, eat and breath predicate logic, paradoxical.  ("Y" is lot more straightforward than "not Y $\implies$ something imcompatible" although, logically, they are equivalent.)
"Because a=b
this means that the single input a gives out 2 different output values, f(a) and f(b)"
$f(a)$ and $f(b)$ are not two different output values.  THey are one output value written two different ways.
∀a∀b(f(a)=f(b)⟺a=b)
This is a fine way to define injectivity but as $a=b \implies f(a) = f(b)$ is always trivially true the bidirection is not nescessary.
