Tao Real analysis: question on function definition (should it be an axiom?)

In Terence Tao's book "Analysis 1", in definition 3.3.1 (function definition), he says

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. Then we define the function $f: X \rightarrow 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.

This definition is on a chapter on set theory foundations, which starts by postulating the existence of objects and sets (he does impure set theory, so not all objects are sets).

Here, under the conditions of the definition, he says that there exists an object $f$, which has the property that for any $x\in X$, $f(x)$ denotes the unique $y\in Y$ such that $P(x,y)$ is true. Shouldn't this be an axiom that postulates the existence of an object?

In another question Equality of functions: axiom or definition? it is said that "Tao does mention that strictly speaking, this definition is an axiom that posits the existence of a function given sets $X,Y$ and property $P$." However, I did not find such a statement in the book.

Solution 1:

Based on Tao’s system, this is a combination of a definition and an axiom.

A more formal treatment would work like this:

Given sets $X$ and $Y$, there is a kind of object called a “function from $X$ to $Y$”. The statement “$f$ is a function from $X$ to $Y$” is denoted $f : X \to Y$.

If $f : X \to Y$ and $x \in X$, then $f(x) \in Y$.

Axiom: Let $P(x, y)$ be a property on $x \in X, y \in Y$. If for all $x \in X$, there is a unique $y \in Y$ such that $P(x, y)$, then there is a function $f : X \to Y$ such that for all $x \in X$, $P(x, f(x))$.

Note that Tao then defines two functions to be equal if their outputs agree.