I recently gave a proof of this theorem:
Every uncountable closed set of reals is in bijection with the reals.
My proof used the axiom of countable choice. Asaf Karagila stated in a comment that Arnie Miller showed in "A Dedekind Finite Borel Set" (Arch. Math. Logic 50, No. 1-2, 1-17 (2011); or on arXiv), that we do not need choice to get perfect subsets of uncountable Borel sets, provided that they can be written as a countable union of $G_δ$ sets, and so the theorem can be proven without choice. But it appears that this proof requires the use of the replacement schema.
So my question is:
Is there a proof of that theorem in Z, namely without replacement or choice? (Z does not have the foundation axiom either, but that seems irrelevant to this theorem.)
If the answer is yes, of course the proof would be interesting.
If the answer is no, it would be equally interesting, as an example of a theorem that can be proven in Z+CC or Z+R despite CC and R both being independent of each other over Z, and apparently unrelated. Also, if the answer is no, I have a follow up question:
Is there a proof of that theorem in Z plus replacement on $ω$? (Namely that the image of any definable function on $ω$ is a set.)