TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-08-06 (claude-opus-5)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

There is exactly one set with no elements, written $\emptyset$

Statement

There is exactly one set with no elements: there is a set $e$ such that $\neg \exists z (z \in e)$ , and any two such sets are equal. That set is written $\emptyset$ .

Facts & Assumptions

Given: the language of set theory, in which the domain of discourse is nonempty (The first-order language of set theory: $\in$ , $=$ , formulas with parameters, and class abbreviations).

[L1]

For any parameters $\overset{ˉ}{p}$ and any set $x$ , there is a set $y$ whose elements are exactly the elements $z$ of $x$ for which $φ (z, \overset{ˉ}{p})$ holds (The Axiom Schema of Separation: for each formula $φ$ , $\forall \overset{ˉ}{p} \forall x \exists y \forall z (z \in y \leftrightarrow (z \in x \land φ (z, \overset{ˉ}{p})))$ ).

[L2]

If every $z$ satisfies $z \in x$ if and only if $z \in y$ , then $x = y$ (The Axiom of Extensionality: $\forall x \forall y (\forall z (z \in x \leftrightarrow z \in y) \to x = y)$ ).

Proof

technique · direct

1.1givenchoose

The domain of discourse is nonempty, so fix a set $a$ .

2.1L1step 1.1

Apply Separation to $a$ with the formula $φ (z) : = \neg (z = z)$ : there is a set $e$ such that, for every $z$ , $z \in e$ holds if and only if $z \in a$ and $\neg (z = z)$ .

3.1step 2.1

No $z$ satisfies $\neg (z = z)$ , so no $z$ satisfies $z \in e$ ; hence $e$ is a set with no elements, which proves existence.

4.1L2step 3.1∎

If $e^{'}$ is also a set with no elements, then $z \in e$ and $z \in e^{'}$ both fail for every $z$ , so $z \in e$ holds if and only if $z \in e^{'}$ , and therefore $e = e^{'}$ ; existence and uniqueness together give the statement, and $\emptyset$ denotes this set.

Remarks

Existence is derived, not assumed. Several presentations take "there is a set with no elements" as an axiom of its own. Here it is a theorem, because the nonemptiness of the domain of discourse is already a validity of first-order logic and Separation converts any set whatever into this one.

There is exactly one set with no elements, written $\emptyset$

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 1 level

Sources

There is exactly one set with no elements, written ∅∅

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 1 level

Sources

There is exactly one set with no elements, written $\emptyset$