Working in first order logic with equality and membership $``\sf FOL(=,\in)"$ Let $\phi x$ be a formula in which only $x$ occur free, and never bound. Let $\psi_i x\vec{z}$ be a formula in which only symbols $``x,z_1,..,z_n"$ occur free, and never bound, such that: $\sf FOL(=,\in)$ $ \vdash \forall \vec{z} \forall x: \psi_i x\vec{z} \to \phi x $ Let $\sf T$ is a theory that extends $\sf FOL(=, \in)$, with only the following axioms: 1. $\exists x. \phi x$ 2. $\forall \vec{z} (\exists x. \psi_{i \leq n} x\vec{z}) $ The idea is that **T** only says that there exists a set that fulfills $\phi$, and stipulate a comprehension axioms assuring the existence of sets satisfying particular finite set of formulas $\psi_1,..,\psi_n$ which are in turn provable to always satisfy $\phi$ in just the background language of **T**. >My question is that given the above conditions, is there a known system that is thought to be a consistent extension of first order logic in which the following is provable? $$\sf Con(\forall x. \phi x) \land Con( T) \\\to Con(T+ \forall x. \phi x)$$. My guess is to the negative, but I don't know of a counter-example.