Axiom ax-regs 35270

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

This axiom is referenced by:  axreg  35271  axregscl  35272