Is it provable in $ZFC$ that if $V_\kappa\vDash ZFC$, then $\kappa$ is strongly inacessible? The other direction of this implication is pretty obvious, but I'm having a hard time seeing why this direction might be true. I suspect that it isn't, but part of my suspicion comes from my inability to cook up a proof to the contrary and that isn't a particularly reliable guide to the truth. Any help is welcome.
 A: No, it is not provable. Quite contrary, it is provably false. More precisely: A cardinal $\kappa$ is worldy iff $V_{\kappa} \models \operatorname{ZFC}$. We can prove that the least worldly cardinal (if any exist) has cofinality $\omega$ and hence is far from being inaccessible.
A: The problematic part is that if $\kappa$ is singular, there might not be any definable first-order function witnessing this. So the only way to find it is essentially to just take the entire power set of $V_\kappa$, and hope to find a short cofinal sequence.
If, however, you replace the schema of Replacement by the second-order statement "For every function $F$ on $V_\kappa$, and every $x$, the range of $F\restriction x$ is a set in $V_\kappa$", then it will be true that $\kappa$ is inaccessible. This is an old theorem of Zermelo, and it is very obvious too now:
If $\kappa$ is not inaccessible then take a function $F\colon\operatorname{cf}(\kappa)\to\kappa$ witnessing this; extend it to be $0$ elsewhere on $V_\kappa$. Now you have a function $F$ and taking $x=\operatorname{cf}(\kappa)$ gives you something that $\operatorname{rng}(F\restriction x)\notin V_\kappa$.
