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)

	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		nfre1	$$⊢Ⅎx\exists x\in z\forall y\in x\neg y\in z$$
9		axreg2	$$⊢x\in z\to \exists x\left(x\in z\wedge \forall y\left(y\in x\to \neg y\in z\right)\right)$$
10		df-ral	$$⊢\forall y\in x\neg y\in z\leftrightarrow \forall y\left(y\in x\to \neg y\in z\right)$$
11	10	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)$$
12		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)$$
13	11 12	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$$
14	9 13	sylib	$$⊢x\in z\to \exists x\in z\forall y\in x\neg y\in z$$
15	8 14	exlimi	$$⊢\exists xx\in z\to \exists x\in z\forall y\in x\neg y\in z$$
16	7 15	vtoclg	$$⊢A\in V\to \left(\exists xx\in A\to \exists x\in A\forall y\in x\neg y\in A\right)$$