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)\!.$$

4more comments