Axiom ax-regs 35060

Description: A strong version of the Axiom of Regularity. It states that if there exists a set with property 𝜑, then there must exist a set with property 𝜑 such that none of its elements have property 𝜑. This axiom can be derived from the axioms of ZF set theory as shown in axregs 35073, but this derivation relies on ax-inf2 9556 and is thus not possible in a finitist context. (Contributed by BTernaryTau, 29-Dec-2025.)

Assertion

Ref	Expression
ax-regs	⊢ (∃𝑥𝜑 → ∃𝑦(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑))))

Distinct variable groups:   𝜑,𝑦,𝑧   𝑥,𝑦,𝑧

Allowed substitution hint:   𝜑(𝑥)

Detailed syntax breakdown of Axiom ax-regs

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3	1, 2	wex 1779	. 2 wff ∃𝑥𝜑
4		vy	. . . . . . 7 setvar 𝑦
5	2, 4	weq 1962	. . . . . 6 wff 𝑥 = 𝑦
6	5, 1	wi 4	. . . . 5 wff (𝑥 = 𝑦 → 𝜑)
7	6, 2	wal 1538	. . . 4 wff ∀𝑥(𝑥 = 𝑦 → 𝜑)
8		vz	. . . . . . 7 setvar 𝑧
9	8, 4	wel 2110	. . . . . 6 wff 𝑧 ∈ 𝑦
10	2, 8	weq 1962	. . . . . . . . 9 wff 𝑥 = 𝑧
11	10, 1	wi 4	. . . . . . . 8 wff (𝑥 = 𝑧 → 𝜑)
12	11, 2	wal 1538	. . . . . . 7 wff ∀𝑥(𝑥 = 𝑧 → 𝜑)
13	12	wn 3	. . . . . 6 wff ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑)
14	9, 13	wi 4	. . . . 5 wff (𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑))
15	14, 8	wal 1538	. . . 4 wff ∀𝑧(𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑))
16	7, 15	wa 395	. . 3 wff (∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑)))
17	16, 4	wex 1779	. 2 wff ∃𝑦(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑)))
18	3, 17	wi 4	1 wff (∃𝑥𝜑 → ∃𝑦(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑))))

This axiom is referenced by:  axreg  35061  axregscl  35062