universes

Axiom. universes
set x → ∃U. set U ∧ univ U ∧ x ∈ U

The axiom of universes. It states that each set is a member of some Grothendieck universe.