# Abstract **LEMMA.** If $M$ is a countable standard model for $\mathrm{ZFC}$ then there exists a countable standard model $N$ for $\mathrm{ZFC}$, which is a generic extension of $M$ such that $\mathrm{HOD}^N=M$. **THEOREM.** Let $\Phi$ be a sentence of $\mathcal{L}_{\mathrm{ZF}}$. Then we have $\mathrm{ZF} \vdash\Phi^{\mathrm{HOD}} \iff \mathrm{ZFC} \vdash\Phi$.