I think you're overthinking the issue. The key sticking point, I suspect, is the following:
We don't have to check whether something is equivalent to an instance of Replacement/Separation, just whether it literally is such an instance. (And to stick the landing, note that for Replacement specifically the apparently-complicated "is a function" bit is built directly into the hypothesis of the instance, so the set of formulas for which there is a corresponding Replacement instances is recursive - namely, it's "all of them.")
Let's think about the Replacement scheme, since that's the one that on the face of it is more complicated. All you have to do is recognize when a sentence $\varphi$ in the language of set theory $\{\in\}$ is an instance of the Replacement scheme. But this is just the task of determining when $\varphi$ has the form $$\forall x_1,..., x_n,a[\forall y(y\in a\implies \exists ! z(\psi(y,z,x_1,...,x_n)))$$ $$\implies\exists w\forall y\exists z(y\in a\implies z\in w\wedge\psi(y,z,x_1,...,x_n))]$$ for some $n$ and some formula $\psi$ with $n+2$ free variables. (OK fine, "$\exists !$" isn't in the syntax of first-order logic, but it's an obvious abbreviation; I'm just using it to keep the above down to reasonable length.) Now here's how we effectively decide whether this holds:
We can effectively enumerate the $\{\in\}$-formulas. This is just saying that the syntax of first-order logic is decidable. Note that this has nothing to do with the meaning of formulas/sentences/etc., I'm just saying we can tell when an expression makes sense.
For each formula $\psi$ we can check whether $\varphi$ is equal to the formula above with that $\psi$. Note that I used the word equal, not equivalent (in whatever sense): I don't have to determine whether a sentence is equivalent to an instance of Replacement, in any sense, just whether it is an instance of Replacement.
So now we just search over all formulas $\psi$ ... of length at most that of $\varphi$. This is a bounded search, so is effective. If we find a $\psi$ of length at most that of $\varphi$ such that $\varphi$ has the form $$\forall x_1,..., x_n,a[\forall y(y\in a\implies \exists ! z(\psi(y,z,x_1,...,x_n)))$$ $$\implies\exists w\forall y\exists z(y\in a\implies z\in w\wedge\psi(y,z,x_1,...,x_n))],$$ we know $\varphi$ is an instance of Replacement; otherwise, we know it isn't, since $\varphi$ can't possibly contain a subformula longer than itself!
We've just seen that the set of sentences which are instances of Replacement is recursive. Similarly, the set of sentences which are instances of Separation is recursive. So here's an algorithm for deciding whether a sentence $\theta$ is an axiom of ZFC:
First, check whether $\theta$ is one of Powerset, Union, Extensionality, Pairing, Foundation, or Choice. If the answer is "yes" for any of these, $\theta$ is a ZFC axiom.
If the answer to all of the above was "no," check whether $\theta$ is a Separation instance. If it is, $\theta$ is a ZFC axiom.
Otherwise, check if $\theta$ is a Replacement instance. If it is, then $\theta$ is a ZFC axiom.
Otherwise, we finally conclude that $\theta$ is not a ZFC axiom.
Now the above is very specific; various related sets are not recursive, namely:
Each of these is r.e. but not recursive, and so we have to be careful to mean exactly what we say: when we say that ZFC is recursively axiomatizable, all we mean is that there is some set of axioms which is recursive and whose deductive closure is that of ZFC.
- Actually this is a bit of an abuse: really we should distinguish between "the deductive closure of ZFC is recursively axiomatizable" and "ZFC itself, as a set of axioms, is recursive. But meh.
