 Transitive closure is Delta-one definable

The transitive closure is obtained by $x_0=x$, $x_{n+1}=\bigcup x_n$, $t={\bigcup }_{n<\omega }{x}_n$. This is transitive, contains $x$ as a subset, and is contained in any other transitive set containing $x$, by induction. Its graph has a Sigma-one formula in set theory saying there exist $\omega$, a sequence with this recursion, and its range. The bounded definition of omega, function and union predicates keep the matrix bounded. Existence and uniqueness in ZF express failure of $y=\mathrm{TC}(x)$ by the existential assertion that the construction produces some $z\ne y$. Thus the graph is a Delta-one formula modulo ZF, and Delta-one absoluteness makes transitive closure absolute between nested transitive models of ZF.