Zermelo–Fraenkel axioms with Choice (ZFC)

The Zermelo–Fraenkel axioms with Choice (ZFC) are a commonly used axiom system for sets and the membership relation $\in$. ZFC consists of the ZF axioms together with the axiom of choice .

A typical presentation includes (informally stated):

• Extensionality: sets with the same elements are equal.
• Empty set: there exists a set with no elements (the empty set ).
• Pairing: for any $a,b$ there is a set containing exactly $a$ and $b$.
• Union: for any set $A$, there is a set whose elements are exactly the elements of elements of $A$ (cf. union ).
• Power set: for any set $A$, there exists the set of all subsets of $A$.
• Infinity: there exists an infinite set (supporting the construction of $\mathbb{N}$).
• Separation schema: subsets defined by a property exist as subsets of an existing set.
• Replacement schema: images of sets under definable functions are sets.
• Foundation (Regularity): every nonempty set has an $\in$-minimal element.

These axioms underlie most of standard mathematics formulated in set-theoretic foundations.