Recall Ackermann set theory. If we extend Ackermann's set theory by adding all axioms of $\sf MK$ to it. We shall denote the universe of all elements by $W$, while $V$ is the primitive constant symbol of Ackermann's set theory denoting the class of all sets [in Ackermann's sense].
Then can we express pure set theoretic definability in $V$ in this theory? That is, can we define the predicate $\operatorname {Vdefinable}_n$ to mean: is a subclass of $V$ that is definable after a set theoretic formula [i.e. not using the primitive constant $V$] from $n$ parameters in $V$? Formally:
$\operatorname {Vdefinable}_n(C) \iff C \subseteq V \land \\\exists \phi \in \operatorname {formulas^{=,\in}} \land \exists x_1,..,x_n \in V : \\\forall y \, (y \in C \iff y \in W \land W \models \phi(x_1,..,x_n,y) )$
The reason why I need that, is to turn the $\omega$-inference rule presented in this prior posting, into ordinary schema.
So first we define:
$\operatorname {Def}_n(V) = \{ C \subseteq V^n \mid \operatorname {Vdefinable}_n (C) \}$,
then we schematize:$$ \forall C \in \operatorname {Def}_n(V) \, \phi \implies \forall C \in \mathcal P(V^n) \, \phi$$; where $\phi$ has all its quantifier's bounded $\in V$, and $V$ doesn't occur in it otherwise, and has only $C$ occurring free.
This schema copies the line of thought about founding Category theory in sets paraphrased as having our cake and eating it too (see Shulman's: Set theory for Category theory. P 27: Strong Reflection Principles)
