Solution (source code)

= Solution

Use the convention that the <transitive closure> $\operatorname{TC}(x)$ is the least <transitive set> containing $x$ as a subset. In <ZF>, <transfinite recursion> and <Axiom schema of replacement> construct
$$
x_0=x,\qquad x_{n+1}=\bigcup x_n,\qquad t=\bigcup_{n<\omega}x_n.
$$
Then $x\subseteq t$. If $a\in b\in t$, some $n$ has $b\in x_n$, whence $a\in x_{n+1}\subseteq t$. Thus $t$ is transitive. If another <transitive set> $s$ contains $x$, induction gives $x_n\subseteq s$ for every $n$, and hence $t\subseteq s$. This proves existence and uniqueness of the <transitive closure>.

Let $W(w)$ be the <bounded definition of omega> above. The displayed construction can be expressed as
$$
\exists w\,\exists f\,\exists r\,\bigl[W(w)\land f:w\to r\land\operatorname{ran}(f)=r\land f(0)=x\land\forall n\in w\,(f(n+1)=\bigcup f(n))\land y=\bigcup r\bigr].
$$
Here the brackets abbreviate a <bounded formula in set theory>: use the permitted bounded function and union predicates, bound the values of $f$ by $r$, and bound each successor index by $w$. Ordered-pair graph access is bounded; $\operatorname{ran}(f)=r$ says every value in $r$ occurs at an index in $w$. Any auxiliary sets used for the graph coding may be put in the initial existential block. Thus this is a <Sigma-one formula in set theory> defining $y=\operatorname{TC}(x)$.

Denote this formula by $T(x,y)$. Existence and uniqueness give the <ZF> equivalence
$$
\neg T(x,y)\iff\exists z\,(T(x,z)\land z\ne y).
$$
The right side is again $\Sigma_1$, after combining existential blocks. Consequently $T$ is a <Delta-one formula modulo ZF>, so <Delta-one absoluteness> applies. Therefore \b[<transitive closure is Delta-one definable> and is ZF-absolute]. If closure is instead required to contain $x$ as an element, apply exactly this construction to $\{x\}$; the absoluteness conclusion is unchanged.