Definition of injective function From wikipedia I obtain the following definition of an injective function :

Let $f$ be a function whose domain is a set $A$. The function $f$ is injective if for all $a$ and $b$ in $A$, if $f(a) = f(b)$, then $a = b$; that is, $f(a) = f(b)$ implies $a = b$. 

From this I conclude that a function $f$ is injective if the below statement is true for all $a,b \in A$:
$$f(a)=f(b) \implies a=b$$
My question is: Can I re-formulate the above statement as $f(a)=f(b) \iff a=b$ ?
 A: Yes, but the implication $a=b\Rightarrow f(a)=f(b)$ holds because you have a function. So in a sense it is redundant. 
That is, "$f$ is a function" implies "$a=b\Rightarrow f(a)=f(b)$". So
$$\begin{align*}
f\text{ is an injective function} &\text{is equivalent to } f\text{ is a function and f is injective}\\
&\text{is equivalent to } f\text{ is a function and } f(a)=f(b)\Rightarrow a=b\\
&\text{implies }\Bigl( (a=b\Rightarrow f(a)=f(b))\text{ and }(f(a)=f(b)\Rightarrow a=b)\Bigr)\\
&\text{is equivalent to } f(a)=f(b)\Leftrightarrow a=b.
\end{align*}$$
Conversely, since "$f$ is a function and $a=b \Rightarrow f(a)=f(b)$" is equivalent to "$f$ is a function", you also have the implication going the other way provided you know that $f$ is a function.
A: Yes.
Let us see why:
$f$ is a function if:


*

*$f\subseteq A\times B$ for some sets $A, B$. That is the elements of $f$ are ordered pairs.

*For all $a\in A$ there exists $b\in B$ such that $(a,b)\in f$.

*For every $a\in A$ if $b,c\in B$ such that $(a,b)\in f$ and $(a,c)\in f$ then $b=c$. We then denote this unique $b$ as $f(a)$.


This means that if $x=y$ then $f(x)=f(y)$ by the definition of a function.
Therefore for injective functions, it is enough to require $f(x)=f(y)\Rightarrow x=y$, since by the definition of $f$ as a function we have the other direction.
A: Yes, you can.  You can formally prove that if a=b, then f(a)=f(b), where f denotes any unary predicate, as follows:
1 |a=b hypothesis
2 |f(a)=f(a) equality (identity) introduction
3 |f(a)=f(b) equality elimination 1, 2, or replacing "a" on the right by "b"
4 If a=b, then f(a)=f(b) 1-3 conditional introduction

So, if f also denotes a function, then a=b implies f(a)=f(b).  Thus, f(a)=f(b)⟹a=b can get reformulated as f(a)=f(b)⟺a=b 
A: Yes. $a=b$ $\Longrightarrow$ $f(a)=f(b)$ means the function $f$ is well-defined.
By definition every function is well-defined.
Example: $f:\mathbb{Q} \to \mathbb{Z}$ "defined" by $f(a/b)=a$ (the numerator "function")
is not well-defined since $4/2=6/3$ but $f(4/2)=4$ and $f(6/3)=6$. The same input gave two different outputs. Thus $f$ is not well-defined. It's not a function!
