It is known that: $ ``\forall x \exists H_x"$, where $H_x$ is defined as the set of all sets hereditarily subnumerous to $x$, is a theorem of $\text{ZF}$. The formal definition of $H_x$ is:

$$H_x=\{y| \forall z \in TC(\{y\}) (\exists f (f:z \to x \wedge f \text{ is injective}))\}$$, where $TC(k)$ stands for the "Transitive closure of($k$)" defined in the standard manner as the minimal transitive superset of $k$.

Question: is $``\forall x \exists H_x"$ a thorem of "$\text{ZF-Regularity + Aczel's anti-foundation axiom}$"?