A possible alternative to the Axioms of Pair, Union, Infinity and Replacement In this question we assume that all formulae are in the language of $\sf ZFC$ and that $\sf ZFC$ is consistent.
Recall that we say that a formula $\varphi(x,y)$ represents a set-like class relation iff for every $x$ the class of all $y$ such that $\varphi(x,y)$ forms a set (for example, $y\in x,\,y\subset x,\,x=y,\,y=\varnothing$ are set-like, but $x\in y,\,x\ne y,\,x=x$ are not).
Consider the following proposition schema (we may call it the Schema of Transitive Closure for set-like relations):

For every set-like relation $\varphi$ and every set $u$ there is a set $v$ that is a superset of $u$ and is closed under $\varphi$. More formally, if $\varphi$ does not have any of the variables $z, u, v$ free,
  $$\forall x\exists z\forall y\left[\varphi(x,y)\Rightarrow y\in z\right]\,\Rightarrow\,\forall u\exists v\left[u\subseteq v\land\forall x\forall y\left(x\in v\land\varphi(x,y)\Rightarrow y\in v\right)\right]$$

If we add this schema as an axiom and drop the usual axioms of Pair, Union, Infinity and Replacement, can we prove the dropped axioms as theorems in this theory? Is this theory equivalent to $\sf ZFC$?
 A: This is certainly a consequence of ZFC: for $\varphi$ set-like and "initial set" $u$, we can define by induction the sets $u_n$ for each $n\in\omega$ as $u_0=u$, $u_{n+1}=u_n\cup\{y: \exists x\in u_n(\varphi(x, y))\}$; and we can show that the sequence $\langle u_i\rangle_{i\in\omega}$ exists (and hence the desired "$u_\omega$") by Replacement.
As to its consequences:


*

*It implies Replacement over $Z$: given an instance $\varphi, u$ of Replacement, consider the formula $\varphi'$ gotten by restricting $\varphi$ to $u$.

*It implies Infinity over $Z-Inf$: take $\varphi$ to define the ordinal successor (if the input is an ordinal, and $0$ otherwise), and apply to $\{\emptyset\}$.
Now let "$(*)$" be "For all $x$, $\{x\}$ is a set." Note that $(*)$ is usually proved by Pairing; in lieu of Pairing, it sees we need $(*)$ to do anything interesting:


*

*It implies Pairing over Separation + $(*)$: given $a, b$, consider $\varphi: x\mapsto b$, applied to $\{a\}$.

*It implies Union over $(*)$ + Separation: consider the formula $\varphi(a, b)\iff b\in a$.
