This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )