$\sf ZF + Def$ is the theory that extends $\mathcal L(=,\in)_{\omega_1,\omega}$ with axioms of $\sf ZF$ (written in $\mathcal L(=,\in)_{\omega, \omega}$) and the axiom of definability:-
$\textbf{Define: } Dx \iff \bigvee x= \{ y \mid \Phi \}$
where $\Phi$ range over all formulas in $\mathcal L(=,\in)_{\omega, \omega}$ in which only the symbol "$y$" occurs free, and the symbol "$y$" never occurs bound.
Axiom of definability: $\forall x Dx$
This theory has its models being exactly the pointwise-definable models of $\sf ZF$ [Hamkins]
Now, if one wants to confine matters to $\mathcal L(=,\in)_{\omega,\omega}$, i.e. the usual $\textbf{FOL}(=,\in)$, then one can add this rule to $\sf ZFC$:
$\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.
This was proved by Hamkins to be equivalent over $\sf ZFC$ to the set theoretic axiom $\sf V=HOD$.
The finitary version of definability doesn't manage to confine all of its models to be the pointwise-definable models of $\sf ZFC$. [see here]. But, it can be argued to be the finitary parallel of the infinitary version.
My question here is:
Are there finitary sentences (i.e. in $\mathcal L(=,\in)_{\omega,\omega}$) that are theorems of $\sf ZF + Def$ yet not provable in $\sf ZFC + \text { Definability rule}$ (or equivalently in $\sf ZFC+[V=HOD])$? Or is the former a conservative extension of the latter?
If there are such sentences, are there clear examples?
