How to interpret the definition of injectivity I am reading Terence Tao's Analysis. In section 3.3, he introduces the definition of injectivity as:

A function f is one-to-one
(or injective) if different elements map to different elements:
$$x \neq x' \Longrightarrow f(x) \neq f(x') $$
Equivalently, a function is one-to-one if
$$ f(x) = f(x') \Longrightarrow x = x'$$

The language is not hard to understand. When I was doing the Exercise 3.3.3, however, I found that it is not very rigorous and different interpretations for the definition result in different conclusions.
For example, if we interpret it as (Suppose the domain is $X$)
$$ \forall x \forall x'(x \in X \wedge x' \in X \wedge (x \neq x' \Longrightarrow f(x) \neq f(x')))$$,
then the empty function is not injective since $x \in \varnothing$ is always a false statement.
On the other hand, if we interpret it as
$$\forall x \forall x'((x \in X \wedge x' \in X \wedge x \neq x') \Longrightarrow (f(x) \neq f(x'))) $$,
or
$$ \forall x \forall x'((x \in X \wedge x' \in X) \Longrightarrow( x \neq x' \Rightarrow (f(x) \neq f(x'))) $$,
then the empty function is always injective for
$$(x \in \varnothing \wedge x' \in \varnothing \wedge x \neq x') \Longrightarrow (f(x) \neq f(x'))$$
and
$$(x \in \varnothing \wedge x' \in \varnothing) \Longrightarrow( x \neq x' \Rightarrow (f(x) \neq f(x'))$$
are vacuously true.
Which of the interpretations is right, or can there be different interpretations for a definition?
 A: If $f$ comes with a domain $X$, then injectivity should be interpreted (in line with your second interpretation):
$$\forall x,x': \left( x \in X \land x' \in X \land x \neq x' \right) \implies (f(x) \neq f(x')$$
which indeed makes any function on an empty domain vacuously injective. The one you mention after, that has two implications, is logically equivalent, as Greg also noted in the comments $p \to (q \to r)$ is logically equivalent to $(p\land q) \to r$.
A: Your first interpretation, $$\forall x\forall x'(x\in X\land x'\in X\land (x\neq x'\to f(x)\neq f(x'))),$$
is incorrect.
What you're trying to do here is to bind the universal quantifier, namely, $$(\forall x\in X)(\forall x'\in X)(x\neq x'\to f(x)\neq f(x')),$$
But a bounded universal quantifier is defined like this: $$(\forall x\in X)\varphi := \forall x(x\in X\to\varphi).$$
The correct interpretation would be the second one indeed, which is $$\forall x\forall x'((x\in X)\to((x'\in X)\to(x\neq x'\to f(x)\neq f(x')))),$$
or after simplifications, $$\forall x\forall x'((x\in X\land x'\in X)\to(x\neq x'\to f(x)\neq f(x'))).$$
Let me just add that in contrast, $(\exists x\in X)\varphi$ is defined as $\exists x(x\in X\land\varphi)$. Which is why you ended up with a problem.
