A question about HOD Suppose $\phi$ is a sentence in the language of ZFC such that ZFC proves $\phi^{HOD}$. I need to show that ZFC already proves $\phi$. Could you give any hints? Thank you!

This might be overkill for this particular problem, but the fact is that we can do class forcing over any model $V$ to produce an extension $V[G]$ such that $\mathrm{HOD}^{V[G]}=V$. This answers your question, since it shows that any model at all is a $\mathrm{HOD}$ of something.
The forcing is closely related to the McAloon-style coding forcing to get $V=\mathrm{HOD}$ and there is a nice exposition in Fuchs, Hamkins, Reitz: Set-Theoretic Geology. The basic idea is to identify a class of nicely behaved cardinals $\delta$ and consider the poset $\mathbb{Q}_\delta$ which generically chooses to make the GCH either hold or fail at $\delta$. The final poset is then the set support $\mathrm{Ord}$-length product $\prod_\delta\mathbb{Q}_\delta$. A density argument shows that any set (of ordinals) in $V$ is coded into the GCH pattern of the final extension and so $V$ is contained in the extension's $\mathrm{HOD}$. The other inclusion follows by a homogeneity argument (there is a slight twist from the way one usually does this since the $\mathbb{Q}_\delta$ are not actually homogeneous).
