Axiom ax-regs 35367

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

This axiom is referenced by:  axreg  35368  axregscl  35369