Why isn't there a need to specify a single $x$ in the axiom schema of replacement? [closed]

The axiom schema of replacement needs a function, defined by ${\forall}y({\exists}x:({\forall}z(P(y,z){\iff}(x=z))))$, where $f(y)=x$.

My question is: why isn't ${\exists}$ replaced by ${\exists}!$?

Shouldn't it be specifically stated that there needs to be only a single $x$, since it's a function.

closed as off-topic by Andrés E. Caicedo, user91500, Watson, JonMark Perry, user223391 Jun 24 '16 at 22:25

This question appears to be off-topic. The users who voted to close gave this specific reason:

• "This question is missing context or other details: Please improve the question by providing additional context, which ideally includes your thoughts on the problem and any attempts you have made to solve it. This information helps others identify where you have difficulties and helps them write answers appropriate to your experience level." – Andrés E. Caicedo, user91500, Watson, JonMark Perry, Community
If this question can be reworded to fit the rules in the help center, please edit the question.

• There is something known as the Axiom Schema of Collection, which you might want to look at. – Transcendental Jun 23 '16 at 20:21
• You already assume that $P$ defines a function. – Asaf Karagila Jun 23 '16 at 20:53

No. The axiom already implies that there's only one such $x$.

Given $y$, let $x$ and $x'$ be elements with ${\forall}z(P(y,z){\iff}(x=z))$ and ${\forall}z(P(y,z){\iff}(x'=z))$. Using $z=x$ in the first statement yields $P(y,x)\iff(x=x)$, and thus $P(y,x)$; then using $z=x$ in the second statement yields $P(y,x)\iff(x'=x)$, and thus $x'=x$.

The idea is that you are defining $f(y)$ to be the unique $x$ such that $P(y,x)$ is true. If it said simply ${\forall}y({\exists}x:P(y,x))$ then you would be right that it needs to say $\exists!$ instead of just $\exists$. But notice that it says not just that there is an $x$ such that $P(y,x)$ but that there is an $x$ such that $P(y,z)\Leftrightarrow z=x$ for all $z$. This means that $P(y,z)$ is true when $z=x$, but it also means that $P(y,z)$ is not true when $z\not=x$. That is, $z=x$ is the only value of $z$ such that $P(y,z)$ is true. This says exactly that the $x$ such that $P(y,x)$ is true is unique.

To put it another way, ${\exists}x:({\forall}z(P(y,z){\iff}(x=z)))$ is just a way of writing $\exists! x: P(y,x)$ without using the symbol $\exists!$ (which is usually not taken as one of the primitive logical symbols).

The full statement of the axiom schema is as follows: given $\varphi(x,y,u)$, $$\forall u(\forall x(\forall a(a\in x\rightarrow\exists y(\varphi(a,y,u)\land\forall z(\varphi(a,z,u)\rightarrow y=z)))\rightarrow\exists w(\forall y(y\in w\leftrightarrow\exists a(a\in x\land\varphi(a,y,u)))))$$

Namely, if $\varphi$ is a formula which defines a function on $x$, then the range of that function, applied to $x$, is a set.

We already assume that for every $a\in x$ there exists a unique $y$ such that $\varphi(a,y)$ (and the fixed parameters).