Is ZF+Omega rule for sets a complete theory? Omega rule for sets$``\omega^{ Set}"$: if $\{\varphi_0(y),\varphi_1(y), \varphi_2(y),...\}$ is the set of all formulas in the language of $ZF$ in one free variable symbol $``y"$, and if $\psi(x)$ is a formula in one free variable symbol $``x"$, then
From: for each $n=0,1,2,3,...; \text{ we have }\forall x \ [x=\{y|\varphi_n(y)\} \to \psi(x) ]$
We Infer:
$\forall x \ [\psi(x)]$

Question: Is $ZF + \omega^{Set}$ complete?

 A: No.  In fact, the set of theorems of $ZF + \omega^{Set}$ is exactly the same as the set of theorems of $ZF+V=HOD$, which is an ordinary recursively axiomatizable first-order theory and is therefore incomplete (assuming ZF is consistent).
First, note that every definable set is ordinal-definable (here and below, "definable" always means without parameters).  Your "$\omega$-rule" then implies that every set is ordinal-definable, so $ZF + \omega^{Set}$ proves $V=HOD$.
Conversely, I claim that every model $M$ of $ZF+V=HOD$ is a model of $ZF + \omega^{Set}$, and so $ZF + \omega^{Set}$ cannot prove any theorems which are not theorems of $ZF+V=HOD$.  To see this, note that first that since $M\vDash V=HOD$ there is a definable (internal) well-ordering of $M$. Now  suppose $\forall x \ [\psi(x)]$ is false in $M$ for some formula $\psi$.  Then there is a definable element $a\in M$ such that $M\vDash\neg\psi(a)$, namely the least such $a$ with respect to the definable well-ordering of $M$.  Say $a$ is defined by the formula $\varphi$.  Then $a=\{y\mid\varphi_n(y)\}$ where $\varphi_n(y)$ is $\forall x(\varphi(x)\rightarrow y\in x)$.  Thus $M\vDash\neg\forall x \ [x=\{y|\varphi_n(y)\} \to \psi(x) ]$.  Since $\psi$ was arbitrary, your $\omega$-rule is sound in $M$ and $M$ is a model of $ZF + \omega^{Set}$.
