I think I proved the following, can you tell me if my proof is correct?
Exercise 23: Show that if $\lambda$ is a regular infinite cardinal then $\langle H_\lambda , \overline{\in} \rangle$ satisfies the Axiom Schema of Replacement.
The definitions are:
$H_\lambda = \{ x : |TC(x)| < \lambda \}$ where $TC$ denotes the transitive closure.
$\overline{\in}$ is used to mean that the relation in $H_\lambda$ is the actual $\in$.
And the Axiom Schema of Replacement says: For each formula $\varphi (x)$ in $L_S$ which does not contain a free occurrence of the variable $y$, the following is an axiom: $\forall a ( \forall x \in a \exists ! y \varphi (x,y) \rightarrow \exists z \forall x \in a \exists y \in z \varphi (x,y))$.
In words: the range of a definable function is a set.
My proof: Let $\lambda$ be an infinite cardinal and let $f$ be a function with domain $x$ and $x \in H_\lambda$. We want to show that the range of $f$ is also in $H_\lambda$. To this end we observe that $H_\lambda \in \mathbf V$ and since $\mathbf V$ is transitive, $x$ is also in $\mathbf V$. Hence we may apply the Axiom Schema of Replacement which we know holds in $\mathbf V$ to obtain that $f[x]$ is a set in $\mathbf V$. It remains to be shown that $f[x] \in H_\lambda$ that is, that $|TC(f[x])| < \lambda$.
Since $\mathrm{cf}(\lambda) = \lambda$ we know that the smallest ordinal $\delta$ such that there is a function $g: \delta \to \lambda$ that is cofinal in $\lambda$ is $\lambda$. Let $g$ be such a function. Then since $|x| < |\lambda|$ it follows that $f$ is bounded by some $\alpha < \lambda$. Since $\alpha$ is transitive we may conclude that if $f[x] \subset \alpha$ then $TC(f[x]) \subset TC(\alpha)$ and hence $|TC(f[x])| < |TC(\alpha)| < \alpha < \lambda$.
Many thanks for your help!