Does ZF prove that a finite subtheory axiomatizes it over transitive proper class models? If  $\text{ZF}$ is consistent, then it is not finitely axiomatizable. For if $\Gamma$ is a finite axiomatization, then $\text{ZF}$ proves by reflection that $\Gamma$ has a set model, and hence (since $\Gamma$ axiomatizes $\text{ZF}$) so does $\Gamma$. By the Second Incompleteness Theorem, $\Gamma$ is inconsistent. This is absurd, since it axiomatizes $\text{ZF}$.
The following therefore intrigues.
Theorem. There is a finite $\Gamma \subseteq \text{ZF}$ such that every transitive proper class model of $\Gamma$ verifies $\text{ZF}$.
I wish to know whether any obstacle prevents formalizing this in $\text{ZF}$. If not, how does that bear on the aforementioned theorem about finite axiomatizability?
For instance, if formalization is possible, it seems to follow that $\text{ZF}$ proves that, if $\text{ZF}$ is consistent, then $\Gamma$ has a model refuting $\text{ZF}$. Else "every model of $\Gamma$ verifies $\text{ZF}$" is consistent with $\text{ZF + Con(ZF)}$, which is absurd since the joint theory proves that $\text{ZF}$ both is and isn't finitely axiomatizable. But that's not very interesting. Perhaps the theorem implies something about nonfirstorderizability of transitivity? Do tell!
Here is a proof, the length of which merits apology. Seems formalizable to me!
Proof. We specify $\Gamma$ in stages. First let it contain all axioms of $\text{ZF}$ besides Comprehension and Replacement. Next let $\Gamma$ contain the finitely many instances of Comprehension and Replacement needed, in addition to the above, to prove the facts invoked below about absoluteness and the cumulative hierarchy. Following Kunen, let $\text{En}(i,X,j)$ be the set of $j$-tuples from $X$ satisfying the $i$th formula in $j$ variables, relativized to $X$. Where $\ast$ denotes concatenation, write $\eta(m,n,s,t,A,B)$ for

$m, n \in \omega \wedge t \in B \wedge A \in B \wedge s \in B^n \wedge s\ast\langle t, A \rangle \in \text{En}(m, B, n+2)$

and $\mu(m,n,s,t,A,B,y)$ for

$m, n \in \omega \wedge t \in B \wedge A \in B \wedge s \in B^n \wedge y \in B \wedge s\ast\langle t, y, A \rangle \in \text{En}(m, B, n+3).$

Finally, let $\Gamma$ contain the instance (+)

$\forall m,n,s,A,B\ \exists y\ \forall t\ [t \in y \leftrightarrow t \in A \wedge \eta(m,n,s,t,A,B)].$

of Comprehension, and the instance (++)

$\forall m,n,s,A,B[\forall t \in A\ \exists!y\ \mu(m,n,s,t,A,B,y) \rightarrow \exists Y\ \forall t \in A\ \exists y \in Y\ \mu(m,n,s,t,A,B,y)]$

of Replacement. Let nothing else be in $\Gamma$.
Now suppose $M$ is a transitive proper class model of $\Gamma$. To prove that $M$ verifies $\text{ZF}$, it suffices to check that it verifies arbitrary instances of Comprehension and Replacement. We do the former; the latter is similar, using (++) in place of (+). Let $\theta(w_1, \dots, w_n, t, A)$ be a formula, and take sets $w_1, \dots, w_n, A$ in $M$. By Comprehension in $V$, let $a$ be the set of all $t \in A$ such that $\theta^M(w_1, \dots, w_n, t, A)$. We aim to show that $a$ is an element of $M$.
Since $M$ is transitive and contains $A$, $a$ is a subset of $M$. And since $M$ verifies $\Gamma$, the tuple $s = \langle w_1, \dots, w_n \rangle$ is in $M$. Define a cumulative hierarchy on $M$ by setting $M_\alpha = M \cap V_\alpha$. By the reflection theorem, take $\beta > \text{max rank}(a, A, s, \omega)$ such that $\theta$ and $\Gamma$ are absolute for $M_\beta$, $M$. Now $M_\beta$ is a transitive model of $\Gamma$ containing $w_1, \dots, w_n, A, s, \omega$, and each element of $a$. Moreover, $M_\beta \in M$, since $M$ thinks $V_\beta$ exists.
By definition of $\text{En}$ there is an integer $q$, the Gödel number of $\theta$, such that $\text{En}(q, M_\beta, n+2)$ is the set of (n+2)-tuple from $M_\beta$ satisfying $\theta^{M_\beta}$. Using (+) in $M$ with $m = q$ and $B = M_\beta$, and computing relativizations and absoluteness with the aid of $\Gamma$, there is $y \in M$ containing precisely the $t \in M$ such that $t \in A \wedge \theta^{M_\beta}(w_1, \dots, w_n, t, A)$. Since $a$ is a subset of $M_\beta$ and $\theta$ is absolute for $M_\beta$, $M$, this $y$ is just $a$. So $a$ is in $M$, as desired.
QED
By the way, the theorem is Exercise 7 in Chapter V of Kunen.
 A: This is a very interesting question, whose answer I find to be quite a subtle but important point. The answer is that it is not possible to formalize the statement in your question in first-order set theory.
To see this, observe first that the theorem you state is actually merely a theorem scheme, asserting of any axiom $\varphi$ of ZFC that any proper class model of $\Gamma$ is also a model of $\varphi$. That is, the theorem proves each instance of ZFC separately to hold in the given class $M$, if it satisfies $\Gamma$. The proof you give appeals at a critical stage to the Reflection theorem, which is also merely a theorem scheme, and this is why we cannot amalgamate the whole argument as one internal induction. Rather, the way to think about it is that the theorem is proved by an induction that takes place in the meta-theory, establishing each meta-theoretical axiom of ZFC to hold in $M$ as a separate claim. Thus, we only conclude that the standard (meta-theoretic) axioms of ZFC hold in $M$, and we may not deduce that $V$ thinks that $M$ satisfies the internal version of ZFC, using the formulas having Gödel codes in $V$. Indeed, because of Tarski's theorem on the non-definability of truth, we have in general no way to express that a given formula coded by a Gödel code is true in a given class, and so no way even to express that a class $M$ satisfies all of (the internal) ZFC, as opposed to expressing this as a scheme.
