Axiom of empty set

The axiom, stated in natural language, is in essence: This formula is a theorem and considered true in every version of set theory.

In many formulations of first-order predicate logic, the existence of at least one object is always guaranteed.

If the axiomatization of set theory is formulated in such a logical system with the axiom schema of separation as axioms, and if the theory makes no distinction between sets and other kinds of objects (which holds for ZF, KP, and similar theories), then the existence of the empty set is a theorem.

The formulation used in the axiom schema of replacement article only allows to construct the image F[a] when a is contained in the domain of the class function F; then the derivation of separation requires the axiom of empty set.

On the other hand, the constraint of totality of F is often dropped from the replacement schema, in which case it implies the separation schema without using the axiom of empty set (or any other axiom for that matter).