Axiom ax-regs 35096

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 35113, but this derivation relies on ax-inf2 9526 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 2111	. . . . . 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  35097  axregscl  35098