Using Replacement to prove transitive closure is a set without recursion

The proof of recursion with which I’m familiar does not use transitive closure. A version of it can be found on-line in Don Monk’s Advanced Set Theory notes, specifically, as Theorem 4.12 in Chapter 4:

Suppose that $\mathbf G$ is a class function with domain the class of all (ordinary) functions. Then there is a unique class function $\mathbf F$ with domain $\mathrm{On}$ such that for every ordinal $\alpha$ we have $\mathbf F(\alpha)=\mathbf G(\mathbf F\upharpoonright\alpha)$.

This starts on page 19. Roughly speaking the proof is by showing that for each ordinal $\alpha$ there is an approximation $f_\alpha$ to $\mathbf F$ with domain $\alpha$, that these approximations are unique, and that they ‘fit together’ properly, so that one may define $\mathbf F(\alpha)$ as $f_{\alpha+1}(\alpha)$.

You employ the following formula:

$$\exists f(x\in\omega\land f\textrm{ is a function }\land\textrm{dom}(f)=x\cup\{x\}\land f(\varnothing)=\{A\}\\\land(\forall m< x)( f(m\cup\{m\})=\bigcup f(m))\land y=f(x))$$

It's easy to check that this function is unique. To prove that it exists proceed by induction on $n$.