Axiom ax-regs 35131

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 35152, but this derivation relies on ax-inf2 9537 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 1780	. 2 wff ∃𝑥𝜑
4		vy	. . . . . . 7 setvar 𝑦
5	2, 4	weq 1963	. . . . . 6 wff 𝑥 = 𝑦
6	5, 1	wi 4	. . . . 5 wff (𝑥 = 𝑦 → 𝜑)
7	6, 2	wal 1539	. . . 4 wff ∀𝑥(𝑥 = 𝑦 → 𝜑)
8		vz	. . . . . . 7 setvar 𝑧
9	8, 4	wel 2112	. . . . . 6 wff 𝑧 ∈ 𝑦
10	2, 8	weq 1963	. . . . . . . . 9 wff 𝑥 = 𝑧
11	10, 1	wi 4	. . . . . . . 8 wff (𝑥 = 𝑧 → 𝜑)
12	11, 2	wal 1539	. . . . . . 7 wff ∀𝑥(𝑥 = 𝑧 → 𝜑)
13	12	wn 3	. . . . . 6 wff ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑)
14	9, 13	wi 4	. . . . 5 wff (𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑))
15	14, 8	wal 1539	. . . 4 wff ∀𝑧(𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑))
16	7, 15	wa 395	. . 3 wff (∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑)))
17	16, 4	wex 1780	. 2 wff ∃𝑦(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑)))
18	3, 17	wi 4	1 wff (∃𝑥𝜑 → ∃𝑦(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑))))

This axiom is referenced by:  axreg  35132  axregscl  35133