Axioms of Extension and Specification

Now that we have a serviceable understanding of the system of logic used in ZFC, we can start introducing axioms and seeing what stems from them.

Axioms

Our first axiom is going to define the most fundamental relationship between sets, equality. We say that a set is purely defined by the elements it contains, so two sets containing the same elements are the same set. This is put into first order logic with the axiom of extensionality.

Axiom of Extensionality

Two sets are equivalent if they have the same elements

\forall A \forall B [\forall x(x \in A \iff x \in B) \implies A = B]

This is a pretty natural axiom, and is used all of the time to prove the uniqueness of a set. The next axiom is going to allow us to create sets at all.

Axiom of Specificication

Definition

The empty set denoted \varnothing is the set containing no elements. Formally

\varnothing = A \iff \forall x (x \not \in A).

Theorem

The empty set exists.

Theorem

The empty set is unique.