Is this set theory equivalent to ZFC?

Question

Consider a variant of set theory with these axioms:

• Extensionality,
• Regularity (foundation),
• Separation,
• Powerset,
• Axiom of Choice, and
• Transitive closure of a set-like relation is set-like. Update: This did not exactly represent what I had in mind, so the corrected version is given on the next line, and its precise formalization is given below. Sorry for my mistake and ensuing confusion.
• The transitive closure of any set under a set-like relation is a set.

Note that it does not explicitly postulate Pairing, Union, Infinity and Replacement.

Question: Is this set theory equivalent to $\mathrm{ZFC}$?

---

Detailed explanation and formalization:

• We use symbol $\prec$ to represent a binary relation. In general, it is a definable class relation, that is a first-order formula with 2 free variables (and, possibly, additional parameters). As usual, we write $a\prec b$ to represent $\prec\!(a,b),$ and we assume that all bound variables in any formula are automatically renamed before a substitution to avoid variable name conflicts that would change its meaning.
• We use “is a set” and “exists” as synonyms; “sethood” and “existence” are also synonyms.
• We write $a\prec b\prec c$ to represent $a\prec b\land b\prec c$. This notation can also mix several different relation symbols, e.g. $a\prec b\in c$.
• When we say that a relation $\prec$ is “set-like”, we mean $$\color{green}{\forall x\,\exists y\,\forall z\left(z\prec x\;\Rightarrow\; z\in y\right)}.$$
• When we say that “$w$ is a superset of the transitive closure of $s$ under the relation $\prec$”, we mean $$\color{maroon}{s\subseteq w\,\land\,\forall u\,\forall v\left(u\prec v\in w\;\Rightarrow\; u\in w\right)}.$$
• We also may rephrase it as “the transitive closure of $s$ under $\prec$ is a subset of $w$” or simply “the transitive closure of $s$ under $\prec$ is a set”. At this point, we do not need to define what “the transitive closure” exactly is, because we are only interested in asserting its sethood, so existence of any its superset $w$ is sufficient for our purposes. I suppose that, when the need arises, “the transitive closure” can be defined as the smallest such set, and can be carved out of its superset using Separation.
• Our last axiom asserts that, provided $\prec$ is a set-like relation, the transitive closure of any set $s$ under that relation $\prec$ is a set. It can be formalized using the following axiom schema where $\prec$ ranges over all binary relations: $$\left(\vphantom{\Large|}\color{green}{\forall x\,\exists y\,\forall z\left(z\prec x\,\Rightarrow\,z\in y\right)}\right)\,\Rightarrow\,\forall s\,\exists w\!\left(\vphantom{\Large|}\color{maroon}{s\subseteq w\,\land\,\forall u\,\forall v\left(u\prec v\in w\,\Rightarrow\,u\in w\right)}\right)\!.$$

Answer 1

Accepting the convention that it is a logical axiom that the universe is nonempty, the answer is yes. We will formalize the transitive closure axiom schema (TC) as follows: for any definable (with parameters) binary relation $R,$ if for all $x,$ $\{y: y R x\}$ is a set, then for all $x,$ there is a set $T$ such that $x \in T$ and $T$ is closed downwards under $R.$ (*) Of course, this can only be weaker than asserting the existence of a minimum such $T.$

For efficiency, we will prove Pairing, Union, Infinity, and Replacement from Extensionality, Separation, and TC.

Pairing: We first note that $\emptyset$ exists by applying separation to an arbitrary set. Next, for all $x,$ $\{x\}$ exists by applying TC to $x$ and the empty relation. Finally, for all $x, y,$ we get $\{x,y\}$ by applying TC to $x$ and the relation defined by $a R b$ iff $b = x$ and $a=y.$

Union: Fix a set $S.$ By Separation and Russell's paradox, there is $x \not \in S.$ Define $R$ by $a R b$ iff $b = x$ and $a \in S$ or $b \in S$ and $a \in b.$ Then we get $\bigcup S$ by applying TC to $x$ and $R.$

Infinity: Define a relation $R$ by $a R b$ iff $a$ and $b$ are natural numbers and $a=b+1.$ Then $\omega$ exists by applying TC to $\emptyset$ and $R.$

Replacement: Fix a set $S$ and a definable function $F.$ Fix $x \not \in S.$ Define $R$ by $a R b$ iff $b=x$ and $a \in S$ or $b \in S$ and $a = F(b).$ Then we get $F"S$ by applying TC to $x$ and $R.$

(*) Note that my formulation of TC only makes sense under the convention that the transitive closure of a relation is reflexive. Without this convention, then it's not clear we can prove the existence of $\{x\}$ from the axioms I specified. Of course, we can prove it exists from Separation and Power Set, which is included in the axioms listed in the question, but that feels overpowered for our purposes.

Edit: The question was updated with the intended formalization of the transitive closure schema. My TC here follows from Vladimir's version plus existence of $\{x\}$ for all $x,$ and the latter follows from Separation and Power Set.