This phenomenon occurs whenever there is a transitive model of ZFC. Suppose that $M$ is a countable transitive model of ZFC. Let $\newcommand\P{\mathbb{P}}\P$ be the Easton-support class product forcing, adding a Cohen subset to every regular cardinal. Let $M[G]$ be a corresponding forcing extension. For each amenable class $I\subseteq\text{Ord}^{M}$, meaning that $\langle M,{\in},I\rangle$ is a model of ZFC in the language with predicate $I$, let us consider the restriction $\P\upharpoonright I$, which restricts the forcing to the cardinals of $I$. There is a corresponding model $M[G\upharpoonright I]$, which is a transitive model of $M[G]$. We can view $M[G\upharpoonright I]$ as a forcing extension of the GBC model in which $I$ is available as a predicate, but then we restrict back down to the first-order ZFC model that results. There are continuum many different amenable classes, since we can force to add a generic class of ordinals, and these are all amenable, and the corresponding models $M[G\upharpoonright I] are distinct. Since there is a splitting tree whose branches are generic for this class forcing, there are continuum many such classes. Most of them will not be definable in $M[G]$, simply because there are too many. So there are numerous $M[G\upharpoonright I]\subset M[G]$ of inner models that are not definable from parameters in the parent model. If $I$ is chosen mutually generic with $G$ as I've described, then the model $M[G]$ will have the inner model as amenable, and so fulfill $\text{ZFC}_I$, making this a dual example of sorts.