Skip to content
Axiomatic Wiki

WTUniqueness of the empty set

Theorem·T01

There is a unique set with no members.

This is the empty set of D002. Moreover this is unique, by Extensionality.
In words
There is a set B such that, for every x, x is not a member of B. This B is unique, and it is called the empty set.
Rests onF02F09F14A01A05A06
Never needed: F03 · F04 · F05 · F06 · F08 · F10 · F11 · F12 · F13 · A02 · A03 · A04 · A07 · A08 · A09 (computed from the citation graph, not asserted).

Proof

  1. 1
    By Infinity there is a set (the axiom asserts the existence of such an ), so there is at least one set to apply Separation to.
  2. 2
    Apply Separation to with the contradictory property , which nothing satisfies. We obtain the set .
  3. 3
    For every , , which never holds; hence . So has no members, and is the empty set of D002.
  4. 4
    For uniqueness: if is any other set with no members, then and have the same (no) members, so by Extensionality . Hence the empty set is unique.
∎

Remarks

Demoted from an axiom: many textbook presentations of ZFC carry "empty set existence" as a separate axiom, but it is derivable from Separation applied to any set that exists (existence being provided by Infinity). The proof needs only the existence clause of Infinity, not its full strength; its real job is establishing a set to which Separation can be applied.
Wikipedia ↗Set.instEmptyCollection ↗
Propose an edit5 published revisions