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	$$⊢\exists x\phi \to \exists y\left(\forall x\left(x=y\to \phi \right)\wedge \forall z\left(z\in y\to \neg \forall x\left(x=z\to \phi \right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		wph	$$wff\phi$$
2	1 0	wex	$$wff\exists x\phi$$
3		vy	$$setvary$$
4	0	cv	$$setvarx$$
5	3	cv	$$setvary$$
6	4 5	wceq	$$wffx=y$$
7	6 1	wi	$$wff\left(x=y\to \phi \right)$$
8	7 0	wal	$$wff\forall x\left(x=y\to \phi \right)$$
9		vz	$$setvarz$$
10	9	cv	$$setvarz$$
11	10 5	wcel	$$wffz\in y$$
12	4 10	wceq	$$wffx=z$$
13	12 1	wi	$$wff\left(x=z\to \phi \right)$$
14	13 0	wal	$$wff\forall x\left(x=z\to \phi \right)$$
15	14	wn	$$wff\neg \forall x\left(x=z\to \phi \right)$$
16	11 15	wi	$$wff\left(z\in y\to \neg \forall x\left(x=z\to \phi \right)\right)$$
17	16 9	wal	$$wff\forall z\left(z\in y\to \neg \forall x\left(x=z\to \phi \right)\right)$$
18	8 17	wa	$$wff\left(\forall x\left(x=y\to \phi \right)\wedge \forall z\left(z\in y\to \neg \forall x\left(x=z\to \phi \right)\right)\right)$$
19	18 3	wex	$$wff\exists y\left(\forall x\left(x=y\to \phi \right)\wedge \forall z\left(z\in y\to \neg \forall x\left(x=z\to \phi \right)\right)\right)$$
20	2 19	wi	$$wff\left(\exists x\phi \to \exists y\left(\forall x\left(x=y\to \phi \right)\wedge \forall z\left(z\in y\to \neg \forall x\left(x=z\to \phi \right)\right)\right)\right)$$