Weakest Hypothesis Needed for Axiom of Replacement

Question

A typical formal statement of the Axiom of Replacement is (leaving out some technical details about extra "parameter variables" that $\phi$ sometimes takes.)

$[\forall x,y,z\ (\phi(x,y) \wedge \phi(x,z) \implies y=z)] \implies [\forall X \exists Y \forall y\ (y \in Y \iff (\exists x \in X)\ \phi(x,y))]$.

The hypothesis "$\forall x,y,z\ (\phi(x,y) \wedge \phi(x,z) \implies y=z)$" states that the relation $\phi$ defines a function: to each $x$ that is related with some $y$, it is related with only one $y$. One tempting revision to express that hypothesis more succinctly is as $\forall x \exists ! y\ \phi(x,y)$. However, this implies something stronger about $\phi$, namely, that it relates every $x$ to some (unique) $y$, whereas the first formulation allows that for some $x$ and all $y$, $\phi(x,y)$ is false.

Can one safely replace the original hypothesis by the revised one, using the following argument? Suppose $\phi$ is not defined for some values of $x$. Then pick some "dummy" $y'$ (such as $\emptyset$) and let $\phi(x,y')$ be true. Then apply the revised axiom to conclude the original version of the axiom, with some technicalities to handle the fact that $Y$ might now include an extra element $y'$. I don't really do set theory, so it's not clear to me exactly what technicalities would pop up and whether they can be handled, possibly using the other axioms.

I've read a lot about different ways to define the Axiom of Replacement, and the related Axiom of Collection, but no one ever seems to state the hypothesis in exactly this way, so I'm wondering if something goes wrong if you try to use this formulation of the axiom.

(Update: question after here answered in comments) For that matter, is the uniqueness of $y$ even required, or could the axiom be revised to $[\forall x \exists y\ \phi(x,y)] \implies [\forall X \exists Y \forall y\ (y \in Y \iff (\exists x \in X)\ \phi(x,y))]$?

Answer 1

Basically, if one is trying axiomatize ZFC, then all these versions of replacement are equivalent modulo the other ZFC axioms, and there is really nothing going on here. The axiom is quite robust and is invariant under these kind of changes. There aren't really any hidden technicalities that cannot be easily overcome. Replacement is equivalent to collection, and for collection, it suffices to say merely, of every $\phi$, that for every set $A$, there is a set $B$ such that for every $a\in A$, if there is a $b$ with $\phi(a,b)$, then there is a $b\in B$ with $\phi(a,b)$. Thus, $\phi$ need neither be total nor functional.

Meanwhile, however, if one is working in a weaker theory, such as ZFC-, meaning ZFC without the power set, then the strength of the axiom becomes sensitive to how it is formulated. For example, without the power set axiom, the replacement axiom scheme and collection are no longer equivalent. This is due to Andrej Zarach, and you can find a proof in my paper What is the theory ZFC without power set? with Gitman and Johnstone. Without the power set axiom, the situation is that replacement is much weaker than you expect. For example, in the version of ZFC- formulated with replacement, one cannot prove that $\omega_1$ is regular, or the Los theorem on ultrapowers and many other things that are provable if one uses collection instead of replacement. Our summary conclusion is that ZFC- is properly formulated with collection instead of replacement, in order for it to prove the things usually desired in this theory.