Theorem zfregcl

Description: The Axiom of Regularity with class variables. (Contributed by NM, 5-Aug-1994) Replace sethood hypothesis with sethood antecedent. (Revised by BJ, 27-Apr-2021) Avoid ax-10 and ax-12 . (Revised by TM, 31-Dec-2025)

	Ref	Expression
Assertion	zfregcl	$$⊢A\in V\to \left(\exists xx\in A\to \exists x\in A\forall y\in x\neg y\in A\right)$$

Proof

Step	Hyp	Ref	Expression
1		eleq2	$$⊢z=A\to \left(x\in z\leftrightarrow x\in A\right)$$
2	1	exbidv	$$⊢z=A\to \left(\exists xx\in z\leftrightarrow \exists xx\in A\right)$$
3		eleq2	$$⊢z=A\to \left(y\in z\leftrightarrow y\in A\right)$$
4	3	notbid	$$⊢z=A\to \left(\neg y\in z\leftrightarrow \neg y\in A\right)$$
5	4	ralbidv	$$⊢z=A\to \left(\forall y\in x\neg y\in z\leftrightarrow \forall y\in x\neg y\in A\right)$$
6	5	rexeqbi1dv	$$⊢z=A\to \left(\exists x\in z\forall y\in x\neg y\in z\leftrightarrow \exists x\in A\forall y\in x\neg y\in A\right)$$
7	2 6	imbi12d	$$⊢z=A\to \left(\left(\exists xx\in z\to \exists x\in z\forall y\in x\neg y\in z\right)\leftrightarrow \left(\exists xx\in A\to \exists x\in A\forall y\in x\neg y\in A\right)\right)$$
8		ax-reg	$$⊢\exists xx\in z\to \exists x\left(x\in z\wedge \forall y\left(y\in x\to \neg y\in z\right)\right)$$
9		df-ral	$$⊢\forall y\in x\neg y\in z\leftrightarrow \forall y\left(y\in x\to \neg y\in z\right)$$
10	9	rexbii	$$⊢\exists x\in z\forall y\in x\neg y\in z\leftrightarrow \exists x\in z\forall y\left(y\in x\to \neg y\in z\right)$$
11		df-rex	$$⊢\exists x\in z\forall y\left(y\in x\to \neg y\in z\right)\leftrightarrow \exists x\left(x\in z\wedge \forall y\left(y\in x\to \neg y\in z\right)\right)$$
12	10 11	bitr2i	$$⊢\exists x\left(x\in z\wedge \forall y\left(y\in x\to \neg y\in z\right)\right)\leftrightarrow \exists x\in z\forall y\in x\neg y\in z$$
13	8 12	sylib	$$⊢\exists xx\in z\to \exists x\in z\forall y\in x\neg y\in z$$
14	7 13	vtoclg	$$⊢A\in V\to \left(\exists xx\in A\to \exists x\in A\forall y\in x\neg y\in A\right)$$