Let $\mathcal Q$ be some qualification on formulas in the first order language of set theory (FOL($\in$)), *that is met by at least one formula*; Let $T$ be the first order set theory whose extra-logical axioms are the following *sole* axiom schema:


$\mathcal Q$-Comprehension schema: if $\phi(y)$ is a formula that meets qualification $\mathcal Q$, in which $x$ doesn't occur, and in which the symbol $y$ occurs free, and only free; then all closures of: $$\exists x \forall y (y \in x \leftrightarrow \phi(y))$$, are axioms.


Now suppose that $T$ is consistent, and that $\psi(x)$ is some formula in one free variable $x$, and $x$ only occur free in it, and suppose that theory $T$ proves that per the same conditions written above for $\mathcal Q$-Comprehension, all closures of following: $$\forall x [\forall y (y \in x \leftrightarrow \phi(y)) \to \psi(x)]$$, are theorems. 



> 
> Would it always follow that: $T + \forall x (\psi(x))$ is consistent?
> 
> 
> 


The other question is:



> 
> If not, then: are there known conditions that if qualifcation $\mathcal Q$ meets then $T + \forall x (\psi(x))$ would be consistent?
> 
> 
> 



What are the known conditions for a restriction on naive comprehension that enables a generalization of a property all so constructed sets meet?
The answer to the first question is no. Suppose no formula meets qualification Q. Let () be x≠x.


The answer when there is at least one formula that meets qualification Q and the language does not have = as a primitive symbol, is still no. Suppose that the only formulas which meet qualification Q are 
(y∈y or not(y∈y)), and ∃u(tr(u)∧∀s(s∈y-->s∈u)∧∃s(s∈u∧empty(s))) where tr(u) is ∀w∀v(w∈u∧v∈w-->v∈u) and empty(w) is ∀x(not(x∈w)(that is y is contained in a transitive set which has an empty set as an element).
By Q-Comprehension, there is an empty set. A universal set(guaranteed to exist by Q-Comprehension) is a transitive set which has an empty set as an element. Let () be ∃t(t∈x). Then for this Q, T is consistent(it holds in the 2 element set {a,b}
with the binary relation E, where E is defined by xEy iff y=b), 
∀[∀(∈↔())→()] is provable from T for all meeting qualification Q, and +∀(()) is not consistent. 


