Proving Axiom Schema of Replacement holds in $H_\lambda$ 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!
 A: Your proof is not good. For example take $x=\{\varnothing\}$ and $f(\varnothing)=\lambda$. Then we have a function whose domain in $H_\lambda$ but certainly its range is not in $H_\lambda$.
Here is a proposed proof:
Let $a\in H_\lambda$ and $\varphi(x,y)$ a functional formula for $x\in a$. That is to say that it is true that for every $x\in a$ there is a unique $y\in H_\lambda$ such that $\varphi(x,y)$ is true. We want to show that there is some $z\in H_\lambda$ such that $y\in z\iff\exists x\in a.\varphi(x,y)$
Let $z=\{y\in H_\lambda\mid\exists x\in a.\varphi(x,y)\}$. We want to show that $z\in H_\lambda$. For this we need to show that $|TC(z)|<\lambda$. Note that if $t\in TC(z)$ then either $t=z$ or there is some $y\in z$ such that $t\in TC(y)$. Therefore, $$|TC(z)|\leq|\bigcup_{y\in z}TC(y)|+1=\sum_{y\in z}|TC(y)|+1$$
However every $z\subseteq H_\lambda$ so $|TC(y)|<\lambda$ and there are at most $|a|$ points in $z$, therefore $|z|\leq|a|<|TC(a)|<\lambda$. Because $\lambda$ is regular the union of $<\lambda$ sets of size $<\lambda$ has size $<\lambda$, that is the entire inequality above is strictly smaller than $\lambda$, and $z\in H_\lambda$ as wanted.

I should also remark that the replacement schema allows parameters, which in this case means parameters from $H_\lambda$, but the above proof is exactly the same.
