Zermelo–Fraenkel set theory is a first-order axiomatic set theory. Under this name are known two axiomatic systems - a system without axiom of choice (abbreviated ZF) and one with axiom of choice (abbreviated ZFC). Both systems are very well known foundational systems for mathematics, thanks to their expressive power. Although different axiomatizations of set theory are possible, ZF and ZFC are unarguably the most common and well-known ones.