Why is there no equivalence in the definition of injection? Everywhere I found that the definition of an injection only uses an implication. However, I can't think a case where if $f$ is an injective function, and if $a = b$, then $f(a) \neq f(b)$. Why do we use an implication ?
 A: If $a = b$, then $f(a) = f(b)$ for any function $f$ by the substitution property of equality. Thus, the implication $a = b \implies f(a) = f(b)$ is a trivial logical tautology that holds for all functions, whether they are injective or not. It is only the reverse implication, $f(a) = f(b) \implies a = b$, that is relevant to the definition of injectivity.
A: You are right: we define $f$ to be injective if
$$
f(a) = f(b) \implies a = b \tag{1}
$$
but we could just as easily say
$$
f(a) = f(b) \iff a = b. \tag{2}
$$
Why is (1) preferred to (2)? One reason, as Ilmari Karonen points out, is that the backwards direction of (2) is true of all functions, and we don't want to include something already true in the definition, as that's redundant.
Another reason is that we want injectivity to be easy to prove. In order to show $f$ is injective, we want to just assume $f(a) = f(b)$ and deduce that $a = b$. If every time we had to prove something was injective we had to show the if and only if, that would be more work for no good reason.
