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 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		nfre1	|- F/ x E. x e. z A. y e. x -. y e. z
9		axreg2	|- ( x e. z -> E. x ( x e. z /\ A. y ( y e. x -> -. y e. z ) ) )
10		df-ral	|- ( A. y e. x -. y e. z <-> A. y ( y e. x -> -. y e. z ) )
11	10	rexbii	|- ( E. x e. z A. y e. x -. y e. z <-> E. x e. z A. y ( y e. x -> -. y e. z ) )
12		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 ) ) )
13	11 12	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 )
14	9 13	sylib	|- ( x e. z -> E. x e. z A. y e. x -. y e. z )
15	8 14	exlimi	|- ( E. x x e. z -> E. x e. z A. y e. x -. y e. z )
16	7 15	vtoclg	|- ( A e. V -> ( E. x x e. A -> E. x e. A A. y e. x -. y e. A ) )