Both of "rely on" and "semantics" are somewhat fluid concepts, but with assuming that we understand them in the most straightforward way: No, formal proofs do not rely on semantics.
Your elaborated question is a bit hard to understand because it is unclear what you mean by "change if the $\phi$'s say yes or no afterwards". There are several different interpretations one could give that:
If you mean that you decide to use a different formula instead of the $\phi$ you originally used, then naturally the proofs you've already constructed are in grave danger of becoming invalid. These proofs are full of $\phi$s -- or perhaps we should clarify what that means, because formal proofs do not really contain the letter "$\phi$". Instead there's some particular sequence of symbols in the language of set theory (such as "(", "$x$", "$y$, "$\neg$", "$\in$", "$\forall$" etc. but not "$\phi$") which appears at various places in the proof, and which, for our own convenience, we choose to call $\phi$ when speaking about the proof.
Now, deciding to use a different formula would amount to seeking out all occurrences of that sequence of symbols in the proof and replace it by a different sequence of symbols. But that is very unlikely to yield a valid proof, because there are probably (except in trivial cases) steps in the proof whose validity depend on the internal structure of $\phi$. For example, if your old $\phi$ had the form $\psi_1\to\psi_2$ (for some formulas $\psi_1$ and $\psi_2$), then there might well be a step in the proof that concludes $\psi_2$ from $\psi_1$ and $\phi$. However, when you replace $\phi$ by $\phi'$ in the proof, that replacement is not going to affect the hypothesis $\psi_1$ or the conclusion $\psi_2$ of that step, because the replacement only does something for the entire sequence of symbols that is $\phi$. And then suddenly you have a purported proof step that concludes $\psi_2$ from $\psi_1$ and $\phi'$, where the new $\phi'$ may have nothing to do with $\psi_1$ or $\psi_2$. Which makes the proof invalid, as a matter of pure syntax.
(Of course one may try to find appropriate substitutions for $\psi_1$ and $\psi_2$ that would make the substituted proof still work, but then what we're really doing is to attempt to adapt the proof rather than continuing to believe in the same proof).
Or perhaps by "change if the $\phi$'s say yes or no" you mean that you keep using the same formula but somehow cause it to have a different truth value? Then of course the syntactical integrity of your existing proofs is unharmed -- but the question instead arises: what is it actually that you imagine doing in order to cause the same $\phi$ have different truth values? This must depend on how you view the semantics of set theory:
If you're a set-theoretic Platonist, you believe that sets have some kind of independent extrinsic existence, and that the purpose of formal proofs is to discover facts about them that were already true, independent of any notion of proof. However, I don't think you're a Platonist, because that would leave you no room to do anything to make $\phi$ mean something different. As before, $\phi$ is some particular sequence of symbols, and each of those symbols already has a definite semantics -- that of "$\neg$" and ")" are given by the rules of propositional calculus, "$\in$" is fixed by what sets are, and the meaning of "$\forall$" is fixed by which sets actually exist (remember, in this paragraph we're pretending to be Platonists), etc.
So we're probably not Platonists. But then the only avaiable way to speak about whether $\phi(x)$ is "true" or not appears to be model theory. In model theory we can speak of an interpretation of the language of set theory, which is the combination of a class of "things" that the variables of set theory range over, and some definite way to decide whether the "$\in$" relation holds between two given "things". Having an interpretation gives a truth value for every (well-formed, closed) formula -- the meaning of "$\forall$" and "$\in$" come from the interpretation itself, and the meanings of all other symbols are fixed by the rules of model theory itself.
In this framework you can indeed change what your $\phi$ means, simply by choosing to consider one interpretation (of the entire language of set theory) rather than another. Will your old proofs still work after the change? Yes they will, provided that you're only considering interpretations where every axiom used in the proof is true. That is the core "soundness" property of first-order logic: If you have a valid formal proof using certain axioms, then in every model where those axioms are true, the conclusion of the proof also happens to be true in that interpretation.
However, of course, if you decide to use an interpretation that doesn't make the axioms true, then all of your proofs from those axioms become irrelevant.