Assume that $\sf ZFC$ has a transitive model, and let $\varphi$ be a $\Sigma_1$-sentence in the language of set theory. Assume that $\varphi$ holds in every transitive model of $\sf ZFC$. Will it follow that $\varphi$ holds in all models of $\sf ZFC$?
Of course the statement isn't true in general for at least $\Pi_1$ sentences (for example, $\sf Con(ZFC)$), and both conclusions are possible if we don't assume the existence of a transitive model, but what is the answer in this setting? Thank you.