# Axiom of Replacement (Question of notation)

For each formula $\phi$ without $Y$ free, the universal closure of the following is an axiom:

$\forall x\in A \exists !y \phi(x,y) \Longrightarrow \exists Y \forall x\in A \exists y\in Y \phi(x,y)$

My question is about the $!$, does that mean that $y$ is bound in $\phi$? What does the exclamation mark mean? Is it there so that $y\ne \{x: x\not\in x \}$? I am confused.

-
"There is a unique" –  Andres Caicedo Aug 31 '13 at 18:02
(But it is not needed, we can relax the requirement to the usual $\exists$, and the new schema is equivalent to this one.) –  Andres Caicedo Aug 31 '13 at 18:03
I see. Thank you that makes things more clear for me. –  Rustyn Aug 31 '13 at 18:06

Rustyn, $\exists !$ is the quantifier "there is a unique". This is just an abbreviation, as it can be defined in terms of the standard quantifiers: $\exists! x\psi(x)$ is just $\exists x(\psi(x)\land\forall y(\psi(y)\to y=x))$.
Anyway, this version of replacement (where the graph of $\phi$ is a "function") is equivalent to the more generous version where the $\exists!$ is replaced by the usual $\exists$ (where the graph of $\phi$ is just a "relation").
Some people prefer the abbreviation $\exists^{=1}$ instead. –  Andres Caicedo Aug 31 '13 at 18:15
It's not clear to me how to derive the "more generous" version from the usual one, at least not without some kind of choice principle. (Sure, we could add more than one $y$ per $x$ to $Y$, but if we add too many of them we risk the result being too large to be a set, don't we?) –  Henning Makholm Aug 31 '13 at 18:18
@HenningMakholm You minimize the rank of the witnesses $y$. (One useful way of thinking of replacement is saying that any function with a set domain has bounded -as opposed to cofinal- range.) –  Andres Caicedo Aug 31 '13 at 18:21