If we add the following $\omega$-inference rule to $\sf ZF$, would that entail the axiom of Choice?
$\textbf{Definability: }$ if $\phi_1,\phi_2, \phi_3,...$ are all formulas in which only symbol "$y$" occurs free, and "$y$" never occur bound, and that doesn't use the symbol "$x$", and $\psi$ is a formula in which only symbol "$x$" occurs free, and "$x$" never occur bound; then:
$\underline {[i=1,2,3,...; \\ \forall x \, (x=\{y \mid \phi_i\} \to \psi)]} \\ \forall x: \psi$
In English: if a parameter free formula holds for all parameter free definable sets, then it holds for all sets.
First notice that "$x$ is ordinal definable" is definable without parameters by the formula "there exists $\alpha$ s.t. $\alpha$ is ordinal and there exists a finite sequence $\overline \beta$ of ordinals and a Godel number $n$ such that $V_\alpha\models'\text{The formula that n represent defines $x$}'$"
From the reflection theorem we know that "$\phi_k$ defines a set $A$" implies that there exists some ordinal $\alpha$ such that $V_\alpha\models '\phi_k\text{ defines $A$}'$, so we can conclude that $$[i=1,2,3,...; \\ \forall x \, (x=\{y \mid \phi_i\} \to \text{$x$ is ordinal definable})]$$
From the $\omega$-rule "Definability" we get $\forall x(\text{$x$ is ordinal definable})$, in other words we have that $V=HOD$.
And $V=HOD$ is in equivalent to "$V$ admits a (definable) global well ordering".