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$ ?

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.

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.

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

An identity of an Elliptical Integral

Let $G$ a group of order $6$. Prove that $G \cong \Bbb Z /6 \Bbb Z$ or $G \cong S_3$. [closed]

$TT^*=T^2$, show that $T$ is self-adjoint

computing $A_2=\sum_{k=1}^{n}\frac{1}{(z_k-1)^2} $ and $\sum_{k=1}^n \cot^2\left( \frac{k\pi}{n+1}\right)$

What is the role of the proof system in a Henkin-proof of Completeness?

$n^3 \equiv n^5 \pmod{12} $?

Proving $P(n) =n^{\phi(n)} \prod\limits_{d \mid n} \left(\frac{d!}{d^d} \right)^{\mu(n/d)}$

Bijection between the reals and the set of permutations of the natural numbers?

Are there sets $A$ and $B$ such that $A \in B$ and $B \in A$?

Sum Involving Bernoulli Numbers : $\sum_{r=1}^n \binom{2n}{2r-1}\frac{B_{2r}}{r}=\frac{2n-1}{2n+1}$

Use an induction argument to prove that for any natural number $n$, the interval $(n,n+1)$ does not contain any natural number.