Theorem bj-axnul 38258

Description: Over the base theory ax-1 6-- ax-5 1945, the axiom of separation implies the weak emptyset axiom.

By "weak emptyset axiom", we mean the axiom asserting existence of an empty set (which can be called "the" empty set when the axiom of extensionality ax-ext 2735 is posited) provided existence of a set (the True truth constant existentially quantified over a fresh variable, extru 2010). This is the conclusion of bj-axnul 38258.

The weak emptyset axiom implies ⊢ (∃𝑥⊤ → ∃𝑦⊤) without DV conditions hence also the same statement as the weak emptyset axiom without DV conditions on 𝑥, but only on 𝑦, 𝑧.

By "axiom of separation", we mean the universal closure of ax-sep 5255, simulated here by its instance with ⊥ substituted for 𝜑 (and with the variable used to assert existence in the weak emptyset axiom substituted for the containing set) as the hypothesis of bj-axnul 38258.

In particular, the axiom of existence extru 2010 and the axiom of separation together imply the emptyset axiom (and conversely, the emptyset axiom implies the axiom of existence).

Note: this theorem does not require a disjointness condition on 𝑦, 𝑧, although both axioms should be stated with all variables disjoint.

This proof only uses an instance of the axiom of separation with a bounded formula, so is valid in a constructive setting (see the CZF section in the "Intuitionistic Logic Explorer" iset.mm). (Contributed by BJ, 8-Mar-2026.) (Proof modification is discouraged.)

Hypothesis

Ref	Expression
bj-axnul.axsep	⊢ ∀𝑥∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ ⊥))

Assertion

Ref	Expression
bj-axnul	⊢ (∃𝑥⊤ → ∃𝑦∀𝑧 ∈ 𝑦 ⊥)

Distinct variable groups:   𝑥,𝑦   𝑥,𝑧

Proof of Theorem bj-axnul

Step	Hyp	Ref	Expression
1		bj-bisimpr 37638	. . . . . 6 ⊢ ((𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ ⊥)) → (𝑧 ∈ 𝑦 → ⊥))
2	1	alimi 1844	. . . . 5 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ ⊥)) → ∀𝑧(𝑧 ∈ 𝑦 → ⊥))
3	2	ralrid 3088	. . . 4 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ ⊥)) → ∀𝑧 ∈ 𝑦 ⊥)
4	3	eximi 1868	. . 3 ⊢ (∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ ⊥)) → ∃𝑦∀𝑧 ∈ 𝑦 ⊥)
5		bj-axnul.axsep	. . 3 ⊢ ∀𝑥∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ ⊥))
6	4, 5	bj-alimii 37702	. 2 ⊢ ∀𝑥∃𝑦∀𝑧 ∈ 𝑦 ⊥
7		bj-spvw 37749	. 2 ⊢ (∃𝑥⊤ → (∃𝑦∀𝑧 ∈ 𝑦 ⊥ ↔ ∀𝑥∃𝑦∀𝑧 ∈ 𝑦 ⊥))
8	6, 7	mpbiri 261	1 ⊢ (∃𝑥⊤ → ∃𝑦∀𝑧 ∈ 𝑦 ⊥)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568  ⊤wtru 1571  ⊥wfal 1582  ∃wex 1812  ∀wral 3080

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3081

This theorem is used by: (None)