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	|- ( E. x ph -> E. y ( A. x ( x = y -> ph ) /\ A. z ( z e. y -> -. A. x ( x = z -> ph ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	|- x
1		wph	|- ph
2	1 0	wex	|- E. x ph
3		vy	|- y
4	0	cv	|- x
5	3	cv	|- y
6	4 5	wceq	|- x = y
7	6 1	wi	|- ( x = y -> ph )
8	7 0	wal	|- A. x ( x = y -> ph )
9		vz	|- z
10	9	cv	|- z
11	10 5	wcel	|- z e. y
12	4 10	wceq	|- x = z
13	12 1	wi	|- ( x = z -> ph )
14	13 0	wal	|- A. x ( x = z -> ph )
15	14	wn	|- -. A. x ( x = z -> ph )
16	11 15	wi	|- ( z e. y -> -. A. x ( x = z -> ph ) )
17	16 9	wal	|- A. z ( z e. y -> -. A. x ( x = z -> ph ) )
18	8 17	wa	|- ( A. x ( x = y -> ph ) /\ A. z ( z e. y -> -. A. x ( x = z -> ph ) ) )
19	18 3	wex	|- E. y ( A. x ( x = y -> ph ) /\ A. z ( z e. y -> -. A. x ( x = z -> ph ) ) )
20	2 19	wi	|- ( E. x ph -> E. y ( A. x ( x = y -> ph ) /\ A. z ( z e. y -> -. A. x ( x = z -> ph ) ) ) )