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 e. V -> ( E. x x e. A -> E. x e. A A. y e. x -. y e. A ) )

Proof

Step	Hyp	Ref	Expression
1		eleq2	|- ( z = A -> ( x e. z <-> x e. A ) )
2	1	exbidv	|- ( z = A -> ( E. x x e. z <-> E. x x e. A ) )
3		eleq2	|- ( z = A -> ( y e. z <-> y e. A ) )
4	3	notbid	|- ( z = A -> ( -. y e. z <-> -. y e. A ) )
5	4	ralbidv	|- ( z = A -> ( A. y e. x -. y e. z <-> A. y e. x -. y e. A ) )
6	5	rexeqbi1dv	|- ( z = A -> ( E. x e. z A. y e. x -. y e. z <-> E. x e. A A. y e. x -. y e. A ) )
7	2 6	imbi12d	|- ( z = A -> ( ( E. x x e. z -> E. x e. z A. y e. x -. y e. z ) <-> ( E. x x e. A -> E. x e. A A. y e. x -. y e. A ) ) )
8		ax-reg	|- ( E. x x e. z -> E. x ( x e. z /\ A. y ( y e. x -> -. y e. z ) ) )
9		df-ral	|- ( A. y e. x -. y e. z <-> A. y ( y e. x -> -. y e. z ) )
10	9	rexbii	|- ( E. x e. z A. y e. x -. y e. z <-> E. x e. z A. y ( y e. x -> -. y e. z ) )
11		df-rex	|- ( E. x e. z A. y ( y e. x -> -. y e. z ) <-> E. x ( x e. z /\ A. y ( y e. x -> -. y e. z ) ) )
12	10 11	bitr2i	|- ( E. x ( x e. z /\ A. y ( y e. x -> -. y e. z ) ) <-> E. x e. z A. y e. x -. y e. z )
13	8 12	sylib	|- ( E. x x e. z -> E. x e. z A. y e. x -. y e. z )
14	7 13	vtoclg	|- ( A e. V -> ( E. x x e. A -> E. x e. A A. y e. x -. y e. A ) )