Set theory uses the formalism of propositional and predicate calculus to assert properties of arbitrary mathematical objects called "sets". A set can be an element of another set, and this relationship is indicated by the symbol. Starting with the simplest mathematical object, called the empty set, set theory builds up more and more complex structures whose existence follows from the axioms, eventually resulting in extremely complicated sets that we identify with the real numbers and other familiar mathematical objects.

A simplistic concept of sets, sometimes called "naive set theory", is vulnerable to a paradox called "Russell's Paradox" (ru), a discovery that revolutionized the foundations of mathematics and logic. Russell's Paradox spawned the development of set theories that countered the paradox, including the ZF set theory that is most widely used and is defined here.

Except for Extensionality, the axioms basically say, "given an arbitrary set x (and, in the cases of Replacement and Regularity, provided that an antecedent is satisfied), there exists another set y based on or constructed from it, with the stated properties". (The axiom of extensionality can also be restated this way as shown by axexte.) The individual axiom links provide more detailed descriptions. We derive the redundant ZF axioms of Separation, Null Set, and Pairing from the others as theorems.

- ZF Set Theory - start with the Axiom of Extensionality
- Introduce the Axiom of Extensionality
- Classes
- Class form not-free predicate
- Negated equality and membership
- Restricted quantification
- The universal class
- Conditional equality (experimental)
- Russell's Paradox
- Proper substitution of classes for sets
- Proper substitution of classes for sets into classes
- Define basic set operations and relations
- Subclasses and subsets
- The difference, union, and intersection of two classes
- The empty set
- The conditional operator for classes
- The weak deduction theorem for set theory
- Power classes
- Unordered and ordered pairs
- The union of a class
- The intersection of a class
- Indexed union and intersection
- Disjointness
- Binary relations
- Ordered-pair class abstractions (class builders)
- Functions in maps-to notation
- Transitive classes

- ZF Set Theory - add the Axiom of Replacement
- ZF Set Theory - add the Axiom of Power Sets
- Introduce the Axiom of Power Sets
- Derive the Axiom of Pairing
- Ordered pair theorem
- Ordered-pair class abstractions (cont.)
- Power class of union and intersection
- The identity relation
- The membership relation (or epsilon relation)
- Partial and total orderings
- Founded and well-ordering relations
- Relations
- The Predecessor Class
- Well-founded induction
- Ordinals
- Definite description binder (inverted iota)
- Functions
- Cantor's Theorem
- Restricted iota (description binder)
- Operations
- Maps-to notation
- Function operation
- Proper subset relation

- ZF Set Theory - add the Axiom of Union
- Introduce the Axiom of Union
- Ordinals (continued)
- Transfinite induction
- The natural numbers (i.e., finite ordinals)
- Peano's postulates
- Finite induction (for finite ordinals)
- Relations and functions (cont.)
- First and second members of an ordered pair
- The support of functions
- Special maps-to operations
- Function transposition
- Curry and uncurry
- Undefined values
- Well-founded recursion
- Functions on ordinals; strictly monotone ordinal functions
- "Strong" transfinite recursion
- Recursive definition generator
- Finite recursion
- Ordinal arithmetic
- Natural number arithmetic
- Equivalence relations and classes
- The mapping operation
- Infinite Cartesian products
- Equinumerosity
- Schroeder-Bernstein Theorem
- Equinumerosity (cont.)
- Pigeonhole Principle
- Finite sets
- Finitely supported functions
- Finite intersections
- Hall's marriage theorem
- Supremum and infimum
- Ordinal isomorphism, Hartogs's theorem
- Hartogs function
- Weak dominance

- ZF Set Theory - add the Axiom of Regularity
- ZF Set Theory - add the Axiom of Infinity
- Introduce the Axiom of Infinity
- Existence of omega (the set of natural numbers)
- Cantor normal form
- Transitive closure
- Rank
- Scott's trick; collection principle; Hilbert's epsilon
- Disjoint union
- Cardinal numbers
- Axiom of Choice equivalents
- Cardinal number arithmetic
- The Ackermann bijection
- Cofinality (without Axiom of Choice)
- Eight inequivalent definitions of finite set
- Hereditarily size-limited sets without Choice