ZF is almost finitely axiomatizable I want to show that there is a finite conjunction $\phi$ of axioms of $ZF$, such that every transitive proper class $M$, which satisfies $\phi$, is already a model of $ZF$.
This is an exercise in Kunen's set theory. There is a hint, it seems to be useful to apply the Reflection principle to the union $M = \cup_{\alpha} M \cap R(\alpha)$. But I don't know with which axioms we can do that (we can only use finitely many!), and why this yields an ordinal which is independent from $M$. Please give me only a hint, because basically I want to solve this on my own, but I don't know how to start with the hint above.
Also, what is the "philosophical" reason that we cannot deduce from this, that $ZF$ is finitely axiomatizable (which is wrong)? I mean I cannot prove that this $\phi$ above proves every axiom, but is there also a deeper reason for this?
EDIT: There was an answer with some hints, but it was deleted...
I still don't know how to produce this strange sentence $\phi$.
 A: Suppose that $M$ satisfies all the easy things like extensionality, pairing, etc., plus $\Delta_0$ separation and suppose also that $M$ thinks for every ordinal $\alpha$ that $V_\alpha$ exists (that is, $V_\alpha^M$ exists in $M$). All this is expressible by a single axiom, but when $M$ is a proper class, it ensures that $M$ satisfies the entire Collection scheme, because for any formula $\varphi(x,y)$ and set $A\in M$ for which we want to collect, we may apply Collection in $V$ to find an ordinal $\alpha$ such that whenever $a\in A$ has $\exists y\varphi(a,y)$ in $M$, then such a $y$ may be found in $V_\alpha$ and hence in $V_\alpha^M$. Thus, $V_\alpha^M$ serves as a collection set inside $M$. Similarly, one can get full Separation in $M$ from $\Delta_0$ Separation (or much less, if you care to optimize it), by applying the Reflection theorem, which allows you to bound all the quantifiers by a suitably large $V_\alpha^M$.
The argument works only when $M$ is a proper class, however, because it appeals to Collection in $V$, and uses that $M$ grows taller than the resulting collection set. This method would break down completely when $M$ is a set, since the collection set in $V$ could be unbounded in $M$. 
A: Martin: Just some hints: You know from a class being transitive and proper that a few axioms already hold, right? 
First, recall that classes are definable in ZF.
The main problem is ensuring that replacement and comprehension hold (since these are the axiom schema). Replacement amounts to showing that any class-definable function with domain a set in the class and range contained in the class is an element of the class. 'Of course', this holds, if you have power set holding. (Right?)
What do you need for comprehension? 
Aside, why doesn't this give you finite axiomatizability of ZF? Because you need to use infinitely many axioms of ZF to prove that the class you obtained is indeed a model of ZF.  
