Substitutional quantification in set theory Is there a unary formula $\phi$ in the language of set theory with the following properties:
(i) $ZFC \vdash (\exists x)\phi(x)$
(ii) for each unary formula $\psi$ in the language of set theory for which $ZFC \vdash (\exists! x)\psi(x)$, we have $ZFC \vdash (\forall x)(\psi(x) \rightarrow \neg \phi(x))$
 A: No, such a formula does not exist. The reason is that in $L$, the constructible universe, there is a definable well-ordering $<_L$ of the universe. Hence, for any formula $\phi$ such that $L\models\exists x\,\phi(x)$, there is a formula $\psi_\phi$ such that $L\models\exists!x\,\psi_\phi(x)$ and $L\models\forall x\,(\psi_\phi(x)\to\phi(x))$, namely, $\psi_\phi(x)$ states that $x$ is the $<_L$-first witness to $\phi$.
Replacing your theory with $\mathsf{ZFC}+V\ne L$ does not help either, as we can always use class forcing to make $V=HOD$, the class of hereditarily ordinal definable elements, in which case we again have a definable well-ordering of the universe.
On the other hand, it is consistent that a formula as you suggest exists. Not provably, of course, as just indicated, but that some model $M$ satisfies the versions of (i) and (ii) in your post with each "$\mathsf{ZFC}\vdash$" replaced with "$M\models$". Namely, let $g$ be a real Cohen generic over $L$, and consider $M=L[g]$ and $\phi(x)$ the statement that $x$ is Cohen-generic over $L$.
