Equality of functions: axiom or definition? I'm studying Tao's Analysis I. He defines functions as objects of a distinct type:

Definition 3.3.1 (Functions). Let $X$, $Y$ be sets, and let $P(x, y)$ be a property pertaining to an object $x \in X$ and an object $y \in Y$, such that for every $x \in X$, there is exactly one $y \in Y$ for which $P(x, y)$ is true (this is sometimes known as the vertical line test).
Then we define the function $f \colon X \to Y$ defined by $P$ on the domain $X$ and range $Y$ to be the object which, given any input $x \in X$, assigns an output $f(x) \in Y$, defined to be the unique object $f(x)$ for which $P(x, f(x))$ is true.
Thus, for any $x \in X$ and $y \in Y$,
$$
y = f(x) \iff P(x, y) \text{ is true.}
$$

Tao does mention that strictly speaking, above is an axiom that posits the existence of a function given sets $X, Y$ and property $P$.
He defines function equality as follows:

Definition 3.3.7 (Equality of functions). Two functions $f \colon X \to Y$, $g\colon X \to Y$ with the same domain and range are said to be equal, $f = g$, if and only if $f(x) = g(x)$ for all $x \in X$.

However, I don't think that one can deduce the following statement using just the above definition:
$$
\text{Let $X$, $X'$, $Y$ be sets and let $f\colon X\to Y$ and $f\colon X'\to Y$. Then $X=X'$.}
$$
I think that this can be fixed if one assumes, instead of the above equality definition, the following axiom, which has the undefined primitive equality:

Axiom. Let $f$ and $g$ be functions. Then $f=g$ if and only if for any sets $X, Y, X', Y'$, if $f\colon X\to Y$ and $g\colon X'\to Y'$, then $X=X'$, $Y=Y'$ and for each $x\in X$, we have $f(x) = g(x)$.

Question: Is the statement that I think is not deducible from the original definitions indeed so? If so, does my axiom really solves the issue?

Another issue:
In my discussion below with Mauro, I realized that there is another issue with the original definition. I'll just quote my comment:

Definition 3.3.7 can say whether functions are equal or not only if one first fixes their domains and codomains. But we don't yet know (just from the original definitions) whether a given function determines its domain and codomain uniquely. And hence we can't conclude whether two functions $f$ and $g$ are equal or not without mentioning their domains and codomains.

 A: Long comment
We may compare the standard set-theoretic definition of function as a set of ordered pair with the following one, from Robert Goldblatt, Topoi : The Categorial Analysis of Logic (2ed. 1984) , page 19:

modify the definition of function in the following way. Firstly for sets $A$ and $B$ we define the product set or Cartesian product of $A$ and $B$ to be the set of all ordered pairs whose first elements are in $A$ and second elements in $B$. This is denoted $A \times B$, and so
$$A \times B = \{ \langle x, y \rangle : x \in A \land y \in B \}.$$
A function is now defined as a triple $f = \langle A, B, R \rangle$, where $R \subseteq A \times B$ is a relation from $A$ to $B$ (the graph of $f$), such that for each $x \in A$ there is one and only one $y \in B$ for which $\langle x, y \rangle \in R$. Thus the domain ($A$) and codomain ($B$) are incorporated in the definition of a function from the outset.

Consider now the following example (taken from the linked post):
\begin{align}f:\{0,1\}&\rightarrow \mathbb{R}\\0&\mapsto2\\1&\mapsto 3\end{align}
and the function \begin{align}f':\{0,1\}&\rightarrow \{2,3\}\\0&\mapsto2\\1&\mapsto 3\end{align}
From the traditional point of view, $f=f'$, because $f= \{ (0,2), (1,3) \}=f'$, while according to Goldblatt's defintion the two objects $\langle \{ 0,1 \}, \mathbb R, f \rangle$ and  $\langle \{ 0,1 \}, \{ 2,3 \}, f' \rangle$ are not the same.
IMO, this one is also Tao's approach.

How does a function uniquely determines its domain?

Via its definition: $\langle X, Y, f \rangle$.
A: I think you are right. Tao's definition 3.3.7, if we take it strictly
as it is, says when two functions with the same domain and range are
equal. It does not say whether two functions with different domains
or different ranges or both, are in some cases equal or, if that never
happens. Thus, you can not deduce $X=X'$, from $f:X\rightarrow Y$
and $f:X'\rightarrow Y$. The definition should say:

Two functions $f$ and $g$ are equal, if and only if they have the
same domain and range and for each $x$ in the domain, we have $f(x)=g(x)$.

But this is equivalent to your axiom, so yes, you have fixed the problem.
I think, what he intends to say in 3.3.7, is the same as the
above, but the way he phrase it is not perfect.
