A set $x$ is hereditarily countable when every membership-descendant of $x$ (including $x$ itself) is countable.
In this paper, Jech proved in ZF that the class of all hereditarily countable sets is a set. (See here and here and here for developments of this result.)
Can this be shown in the variant of ZF that uses Aczel's Antifoundation instead of Foundation?
Another question that I think is equivalent: does ZF prove the existence of a final coalgebra for the countable powerset functor?
Update. This answer does not answer the question that was asked, since Jech is using what had seemed to me as an idiosyncratic definition of hereditary countable. But upon reflection, I find his definition completely natural in a context without AC. Namely, he defines that a set is hereditary countable when it is countable and every element of the transitive closure is countable. In short, the set itself and every set appearing hereditarily in it is countable. (This is not equivalent, even in ZF as Jech proves, to saying that the transitive closure of the set is countable.)
If a negative answer to the question is possible, I suspect it will arise by finding a model of ZF in which AC fails badly and using it to interpret a model of ZFA where there is proper class of inequivalent accessible pointed graphs such that every node has only countably many children. I have wondered whether Gitik's model, in which every infinite limit ordinal has cofinality $\omega$, will be helpful for this.
Original answer:
In ZFA every set is determined by the underlying accessible pointed graph, the $\in$ relation on the transitive closure, and the AFA axiom asserts that isomorphic graphs will give rise to the same set.
Thus, the hereditarily countable sets will arise from the countable graphs, which is a set by the argument you mentioned. And so in ZFA the hereditarily countable sets will form a set.
It is interesting to note that, being countable, the underlying graphs of any hereditarily countable set can be realized within the well-founded part of the universe, even if the set that they name is not well-founded. So the hereditarily countable sets in ZFA arise from a functional image of the well-founded hereditarily countable sets, namely, the graph relations on $\omega$.
This argument doesn't work at all in the Boffa antifoundation theory, which has a proper class of distinct Quine atoms, all of which are countable. However, even in that theory, there are up to isomorphism only a set of hereditarily countable sets, since they are determined up to isomorphism by the underlying graph relation.
