Let $\phi$ be a ZFC formula and $\lceil \phi \rceil$ its syntactic representation.
Suppose that
- ZFC proves that "if $\phi$ then there exists a string $x$ that represents a ZFC proof of $\lceil \neg \phi \rceil$ in some suitable proof system" ($x \equiv \lceil ZFC \vdash ^* \neg \phi \rceil$)
Can we conclude (by contradiction) that:
- ZFC proves $\neg \phi$
Here is a rather general answer. Let $T$ be any theory which is subject to the Godel's incompleteness theorems (for example, $T$ might be ZFC, as in the question, or ZFC+Con(ZFC) as discussed in the comments). Let $\phi$ be the statement "$T$ is inconsistent". Clearly $\phi$ implies that $T$ proves $\neg\phi$ (indeed, inconsistency of $T$ implies that $T$ proves anything). On the other hand, $T$ can't prove $\neg\phi$, because of the second incompleteness theorem. Hence we can't make the inference you are asking about.