Theorem bj-axnul 37276

Description: Over the base theory ax-1 6-- ax-5 1911 plus the axiom of separation (the universal closure of ax-sep 5241), simulated here by its instance with ⊥ substituted for 𝜑 as an antecedent, the existence axiom extru 1976 is equivalent to the existence of an empty set (which can be called "the" empty set once ax-ext 2708 is assumed). The present proof proves only one implication, but the reverse implication is straightforward (though not expressible in this closed form since it involves another instance of the existence axiom). This proof only uses an instance of the axiom of separation with a bounded formula, so is valid in CZF (see the corresponding section in the "Intuitionistic Logic Explorer" iset.mm). (Contributed by BJ, 8-Mar-2026.) (Proof modification is discouraged.)

Assertion

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

Distinct variable groups:   𝑥,𝑦   𝑥,𝑧

Proof of Theorem bj-axnul

Step	Hyp	Ref	Expression
1		biimp 215	. . . . . . 7 ⊢ ((𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ ⊥)) → (𝑧 ∈ 𝑦 → (𝑧 ∈ 𝑥 ∧ ⊥)))
2		falimd 1559	. . . . . . 7 ⊢ ((𝑧 ∈ 𝑥 ∧ ⊥) → (𝑧 ∈ 𝑦 → ⊥))
3	1, 2	syli 39	. . . . . 6 ⊢ ((𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ ⊥)) → (𝑧 ∈ 𝑦 → ⊥))
4		dfnot 1560	. . . . . 6 ⊢ (¬ 𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑦 → ⊥))
5	3, 4	sylibr 234	. . . . 5 ⊢ ((𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ ⊥)) → ¬ 𝑧 ∈ 𝑦)
6	5	alimi 1812	. . . 4 ⊢ (∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ ⊥)) → ∀𝑧 ¬ 𝑧 ∈ 𝑦)
7	6	eximi 1836	. . 3 ⊢ (∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ ⊥)) → ∃𝑦∀𝑧 ¬ 𝑧 ∈ 𝑦)
8	7	alimi 1812	. 2 ⊢ (∀𝑥∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ ⊥)) → ∀𝑥∃𝑦∀𝑧 ¬ 𝑧 ∈ 𝑦)
9		bj-spvw 37274	. 2 ⊢ (∃𝑥⊤ → (∀𝑥∃𝑦∀𝑧 ¬ 𝑧 ∈ 𝑦 → ∃𝑦∀𝑧 ¬ 𝑧 ∈ 𝑦))
10	8, 9	syl5com 31	1 ⊢ (∀𝑥∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ ⊥)) → (∃𝑥⊤ → ∃𝑦∀𝑧 ¬ 𝑧 ∈ 𝑦))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1539  ⊤wtru 1542  ⊥wfal 1553  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781

This theorem is referenced by: (None)