Axiom ax-regs

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	⊢ 𝑥
1		wph	⊢ 𝜑
2	1 0	wex	⊢ ∃ 𝑥 𝜑
3		vy	⊢ 𝑦
4	0	cv	⊢ 𝑥
5	3	cv	⊢ 𝑦
6	4 5	wceq	⊢ 𝑥 = 𝑦
7	6 1	wi	⊢ ( 𝑥 = 𝑦 → 𝜑 )
8	7 0	wal	⊢ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 )
9		vz	⊢ 𝑧
10	9	cv	⊢ 𝑧
11	10 5	wcel	⊢ 𝑧 ∈ 𝑦
12	4 10	wceq	⊢ 𝑥 = 𝑧
13	12 1	wi	⊢ ( 𝑥 = 𝑧 → 𝜑 )
14	13 0	wal	⊢ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 )
15	14	wn	⊢ ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 )
16	11 15	wi	⊢ ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) )
17	16 9	wal	⊢ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) )
18	8 17	wa	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) )
19	18 3	wex	⊢ ∃ 𝑦 ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) )
20	2 19	wi	⊢ ( ∃ 𝑥 𝜑 → ∃ 𝑦 ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ) )