In ZF (or at least the formulation I'm studying), the empty set axiom [tex](\exists \phi)(\forall z)(\neg (z\in \phi)) [/tex] is a consequence of the other axioms, namely the axiom of infinity (and separation, though googling says that's not necessary) which is [tex](\exists x) (p)[/tex] where p is some formula to guarantee the infinite set is what we want. Let's assume the axiom of separation (subset making) too. Here are my questions: When they say that the Empty Set Axiom is a theorem in ZF, does that mean we can prove it using first order logical axioms and deductions (axioms like p=> (q=>p))? Does anyone know of such a proof, if so? The empty set is included in the 'p' of the Axiom of Infinity - though I'm guessing the Axiom of Infinity doesn't actually require it (immediately) to be empty. Assuming the Axiom of Separation, [tex](\forall x)(\exists y) (\forall z)(z\in y <=> z\in x \wedge q(z))[/tex] can we just pick q(z)="z not in x" and let x be the set discussed in the Axiom of infinity? If so, how do we formalize this? Thanks. And sorry if it's in the wrong forum.