This post is actually related to posting titled What is the strength of definable ZFC?. However the presentation there was 'semiformal', and here I'll present a complete formal exposition of that theory.
To the language of ZFC minus Power, lets add a primitive one place predicate symbol $``definable"$, and lets add the following Omega inference rule:
if $\{\phi_1(y),\phi_2(y),\phi_3(y),...\}$ is the set of ALL formulae in the language of ZFC, in just one free variable symbol $``y"$; and if $\psi(X,w_1,..,w_m)$ is a formula in the language of ZFC, in which all and only symbols $``X,w_1,..,w_m"$ occur free, then:
\begin{equation} \text{ for each m=0,1,2,...; $w_1,..,w_m$ } \begin{cases} \forall X\ [\forall y (y \in X \leftrightarrow \phi_1(y))\to \psi(X,w_1,..,w_m)]\\ \forall X\ [\forall y (y \in X \leftrightarrow \phi_2(y))\to \psi(X,w_1,..,w_m)]\\ \forall X\ [\forall y (y \in X \leftrightarrow \phi_3(y))\to \psi(X,w_1,..,w_m)]\\ \ . \\ \ . \\ \ . \\ \rule{10,cm}{1,pt} \\ \forall X [definable(X) \to \psi(X,w_1,..,w_m)] \\ \end{cases} \end{equation}
This is a schema of inference rules whose antecedent is also schema! It means for each particular substitution of $m$ and $w_1,..,w_m$: if ALL sentences $``\forall X\ [\forall y (y \in X \leftrightarrow \phi_n(y))\to \psi(X,w_1,..,w_m)]"$, where $n=1,2,3,...$; were fulfilled! Then we infer the sentence below the line.
This would ensure that every set $x$ that fulfills the predicate "$definable$" is a set definable after a parameter free formula in the language of ZFC.
Proof: suppose there exists a set $s$ that is not parameter free definable, then take $m=1$ and substitute $w_1$ by $s$, and run the omega rule above for the formula $\psi(X,w_1)$ being the formula $X \neq s$, the antecedent schema would be fulfilled, and so by that omega rule, we infer that every definable set $X$ must satisfy $X \neq s$
Add the axiom scheme of definability: if $\phi(y)$ is a formula in the langauge of ZFC, in which only the symbol $``y"$ occurs free, then: $$\forall X\ [\forall y (y \in X \leftrightarrow \phi(y))\to definable(X)]$$; is an axiom
From the above omega rule and the definability axiom scheme, the equivalence of the predicate $definable$ with definability after a parameter free formula in the language of ZFC is established!
Now to ZFC minus power, lets add the "definable power set axiom" that is:
$\forall A \exists x \forall y \ [y \in x \leftrightarrow y \subseteq A \wedge definable(y)]$
Question: Would that theory still interpret ZFC over the hereditarily definable realm of this theory?