Let $a$, $b$, $S$ denote sets, and let $\varphi$ be a statement in two set variables. Here are two ways of expressing the Axiom of Replacement which I have seen used:
1) If $$\text{for all } a \in S, \text{ we have that } \exists \, b \text{ s.t. } \varphi(a,b) \text{ is true, and } \varphi(a,b) \, \& \, \varphi(a,c) \Rightarrow b = c,$$ then $$\text{there exists } T, \text{ such that for all } b, \text{ we have } b \in T \, \text{iff} \, \exists \, a \in S \text{ s.t. } \varphi(a,b).$$
2) If $$\text{for all } a \in S, \text{ we have that } \varphi(a,b) \, \& \, \varphi(a,c)\Rightarrow b = c,$$ then $$\text{there exists } T, \text{ such that for all } b, \text{ we have } b \in T \, \text{iff} \, \exists \, a \in S \text{ s.t. } \varphi(a,b).$$
The first formulation seems to be the more popular one in modern books, though the second one was used in Suppes' Axiomatic Set Theory. My question is whether or not these two formulations are equivalent, assuming only the axiom of extensionality as set theory background. Obviously 2) implies 1), but the converse implication is not so obviously true or false to me. Any help would be appreciated.
I'm going to work with the parameterised versions of (1) and (2) for simplicity.
As the following theorems show, (1) and (2) are equivalent in the presence of the empty set axiom, but they can fail to be equivalent without it.
${\bf Theorem}$ (Extensionality + Emptyset) (1) is equivalent to (2).
${\it Proof.}$ Since you've already pointed out that (2) implies (1), I'll show that (1) implies (2). Assume the antecedent of (2). There are two cases to consider. Either $\exists y\exists x\in S\phi(x, y)$ or not. If not, then:
$\{y:\exists x\in S\phi(x, y)\} = \emptyset$
and we're done. So suppose $t$ is such that $\phi(x, t)$ for some $x\in S$. Now consider the condition:
$\psi = [\exists y\phi(x, y) \to \phi(x, y)] \wedge [\neg\exists y\phi(x, y) \to y = t]$.
It is straightforward to check that $\psi$ satisfies the antecedent of (1), so we can use it to get:
$\{y: \exists x\in S\psi(x, y)\} = \{y: \exists x\in S \phi(x, y) \vee y = t\} = \{y: \exists x\in S \phi(x, y)\}$
as required. $\Box$
${\bf Theorem}$ (2) doesn't follow from the theory consisting of (1), Extensionality, Pairing, Union, Powerset, AC, and Infinity (in the form: there's a set which is injectable into a proper subset of itself).
${\it Proof}$ ${\it sketch.}$ Take a non-well-founded omega sequence $x_0 = \{x_1\} \wedge x_1 = \{x_2\},... \wedge$ $x_{n+1} = \{x_ n\}$. Then we build the cumulative hierarchy on top of it. For instance, for any $\alpha$ we let $D_{\alpha + 1} = \mathcal P(D_\alpha)\setminus\{\emptyset\}$ and $D_\lambda = \bigcup_{\alpha<\lambda} D_\alpha$ for limits $\lambda$. For an inaccessible $\kappa$, it is straightforward to verify that $D_\kappa$ satisfies (1), Extensionality, Pairing, Union, Powerset, AC, and Infinity. It is also easy to see that it doesn't contain an empty set. But (2) implies the existence of an empty set. $\Box$
It's perhaps worth noting that this model also satisfies a restricted version of Separation, namely:
$\exists x\in y\cap \phi \to \{x\in y:\phi\}$ exists.
So there's a sense in which we can have all of ZFC$^-$ (i.e. ZFC - Foundation) just short of having the empty set axiom without also having (2).
${\bf Question.}$ Are there models of ZFC with the modified versions of Infinity and Separation which fail to satisfy (2)?