Metamath Proof Explorer

Theorem axregnd

Description: A version of the Axiom of Regularity with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 3-Jan-2002) (Proof shortened by Wolf Lammen, 18-Aug-2019) (New usage is discouraged.)

Ref Expression
Assertion axregnd 
|- ( x e. y -> E. x ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) )

Proof

Step Hyp Ref Expression
1 axregndlem2 
 |-  ( x e. y -> E. x ( x e. y /\ A. w ( w e. x -> -. w e. y ) ) )
2 nfnae 
 |-  F/ x -. A. z z = x
3 nfnae 
 |-  F/ x -. A. z z = y
4 2 3 nfan 
 |-  F/ x ( -. A. z z = x /\ -. A. z z = y )
5 nfnae 
 |-  F/ z -. A. z z = x
6 nfnae 
 |-  F/ z -. A. z z = y
7 5 6 nfan 
 |-  F/ z ( -. A. z z = x /\ -. A. z z = y )
8 nfcvf 
 |-  ( -. A. z z = x -> F/_ z x )
9 8 nfcrd 
 |-  ( -. A. z z = x -> F/ z w e. x )
10 9 adantr 
 |-  ( ( -. A. z z = x /\ -. A. z z = y ) -> F/ z w e. x )
11 nfcvf 
 |-  ( -. A. z z = y -> F/_ z y )
12 11 nfcrd 
 |-  ( -. A. z z = y -> F/ z w e. y )
13 12 nfnd 
 |-  ( -. A. z z = y -> F/ z -. w e. y )
14 13 adantl 
 |-  ( ( -. A. z z = x /\ -. A. z z = y ) -> F/ z -. w e. y )
15 10 14 nfimd 
 |-  ( ( -. A. z z = x /\ -. A. z z = y ) -> F/ z ( w e. x -> -. w e. y ) )
16 elequ1 
 |-  ( w = z -> ( w e. x <-> z e. x ) )
17 elequ1 
 |-  ( w = z -> ( w e. y <-> z e. y ) )
18 17 notbid 
 |-  ( w = z -> ( -. w e. y <-> -. z e. y ) )
19 16 18 imbi12d 
 |-  ( w = z -> ( ( w e. x -> -. w e. y ) <-> ( z e. x -> -. z e. y ) ) )
20 19 a1i 
 |-  ( ( -. A. z z = x /\ -. A. z z = y ) -> ( w = z -> ( ( w e. x -> -. w e. y ) <-> ( z e. x -> -. z e. y ) ) ) )
21 7 15 20 cbvald 
 |-  ( ( -. A. z z = x /\ -. A. z z = y ) -> ( A. w ( w e. x -> -. w e. y ) <-> A. z ( z e. x -> -. z e. y ) ) )
22 21 anbi2d 
 |-  ( ( -. A. z z = x /\ -. A. z z = y ) -> ( ( x e. y /\ A. w ( w e. x -> -. w e. y ) ) <-> ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) ) )
23 4 22 exbid 
 |-  ( ( -. A. z z = x /\ -. A. z z = y ) -> ( E. x ( x e. y /\ A. w ( w e. x -> -. w e. y ) ) <-> E. x ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) ) )
24 1 23 syl5ib 
 |-  ( ( -. A. z z = x /\ -. A. z z = y ) -> ( x e. y -> E. x ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) ) )
25 24 ex 
 |-  ( -. A. z z = x -> ( -. A. z z = y -> ( x e. y -> E. x ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) ) ) )
26 axregndlem1 
 |-  ( A. x x = z -> ( x e. y -> E. x ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) ) )
27 26 aecoms 
 |-  ( A. z z = x -> ( x e. y -> E. x ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) ) )
28 19.8a 
 |-  ( x e. y -> E. x x e. y )
29 nfae 
 |-  F/ x A. z z = y
30 elirrv 
 |-  -. z e. z
31 elequ2 
 |-  ( z = y -> ( z e. z <-> z e. y ) )
32 30 31 mtbii 
 |-  ( z = y -> -. z e. y )
33 32 a1d 
 |-  ( z = y -> ( z e. x -> -. z e. y ) )
34 33 alimi 
 |-  ( A. z z = y -> A. z ( z e. x -> -. z e. y ) )
35 34 anim2i 
 |-  ( ( x e. y /\ A. z z = y ) -> ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) )
36 35 expcom 
 |-  ( A. z z = y -> ( x e. y -> ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) ) )
37 29 36 eximd 
 |-  ( A. z z = y -> ( E. x x e. y -> E. x ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) ) )
38 28 37 syl5 
 |-  ( A. z z = y -> ( x e. y -> E. x ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) ) )
39 25 27 38 pm2.61ii 
 |-  ( x e. y -> E. x ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) )