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

Metamath Proof Explorer

Theorem zfregclOLD

Description: Obsolete version of zfregcl as of 31-Dec-2025. (Contributed by NM, 5-Aug-1994) Replace sethood hypothesis with sethood antecedent. (Revised by BJ, 27-Apr-2021) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion zfregclOLD 
|- ( 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 ) )