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

Metamath Proof Explorer

Theorem axregndlem2

Description: Lemma for 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 Mario Carneiro, 10-Dec-2016) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 axreg2 
 |-  ( w e. y -> E. w ( w e. y /\ A. z ( z e. w -> -. z e. y ) ) )
2 1 ax-gen 
 |-  A. w ( w e. y -> E. w ( w e. y /\ A. z ( z e. w -> -. z e. y ) ) )
3 nfnae 
 |-  F/ x -. A. x x = y
4 nfnae 
 |-  F/ x -. A. x x = z
5 3 4 nfan 
 |-  F/ x ( -. A. x x = y /\ -. A. x x = z )
6 nfcvd 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/_ x w )
7 nfcvf 
 |-  ( -. A. x x = y -> F/_ x y )
8 7 adantr 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/_ x y )
9 6 8 nfeld 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x w e. y )
10 nfv 
 |-  F/ w ( -. A. x x = y /\ -. A. x x = z )
11 nfnae 
 |-  F/ z -. A. x x = y
12 nfnae 
 |-  F/ z -. A. x x = z
13 11 12 nfan 
 |-  F/ z ( -. A. x x = y /\ -. A. x x = z )
14 nfcvf 
 |-  ( -. A. x x = z -> F/_ x z )
15 14 adantl 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/_ x z )
16 15 6 nfeld 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x z e. w )
17 15 8 nfeld 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x z e. y )
18 17 nfnd 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x -. z e. y )
19 16 18 nfimd 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x ( z e. w -> -. z e. y ) )
20 13 19 nfald 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x A. z ( z e. w -> -. z e. y ) )
21 9 20 nfand 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x ( w e. y /\ A. z ( z e. w -> -. z e. y ) ) )
22 10 21 nfexd 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x E. w ( w e. y /\ A. z ( z e. w -> -. z e. y ) ) )
23 9 22 nfimd 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x ( w e. y -> E. w ( w e. y /\ A. z ( z e. w -> -. z e. y ) ) ) )
24 simpr 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> w = x )
25 24 eleq1d 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( w e. y <-> x e. y ) )
26 nfcvd 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/_ z w )
27 nfcvf2 
 |-  ( -. A. x x = z -> F/_ z x )
28 27 adantl 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/_ z x )
29 26 28 nfeqd 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ z w = x )
30 13 29 nfan1 
 |-  F/ z ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x )
31 24 eleq2d 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( z e. w <-> z e. x ) )
32 31 imbi1d 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( ( z e. w -> -. z e. y ) <-> ( z e. x -> -. z e. y ) ) )
33 30 32 albid 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( A. z ( z e. w -> -. z e. y ) <-> A. z ( z e. x -> -. z e. y ) ) )
34 25 33 anbi12d 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( ( w e. y /\ A. z ( z e. w -> -. z e. y ) ) <-> ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) ) )
35 34 ex 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> ( w = x -> ( ( w e. y /\ A. z ( z e. w -> -. z e. y ) ) <-> ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) ) ) )
36 5 21 35 cbvexd 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> ( E. w ( w e. y /\ A. z ( z e. w -> -. z e. y ) ) <-> E. x ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) ) )
37 36 adantr 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( E. w ( w e. y /\ A. z ( z e. w -> -. z e. y ) ) <-> E. x ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) ) )
38 25 37 imbi12d 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( ( w e. y -> E. w ( w e. y /\ A. z ( z e. w -> -. z e. y ) ) ) <-> ( x e. y -> E. x ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) ) ) )
39 38 ex 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> ( w = x -> ( ( w e. y -> E. w ( w e. y /\ A. z ( z e. w -> -. z e. y ) ) ) <-> ( x e. y -> E. x ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) ) ) ) )
40 5 23 39 cbvald 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> ( A. w ( w e. y -> E. w ( w e. y /\ A. z ( z e. w -> -. z e. y ) ) ) <-> A. x ( x e. y -> E. x ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) ) ) )
41 2 40 mpbii 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> A. x ( x e. y -> E. x ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) ) )
42 41 19.21bi 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> ( x e. y -> E. x ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) ) )
43 42 ex 
 |-  ( -. A. x x = y -> ( -. A. x x = z -> ( x e. y -> E. x ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) ) ) )
44 elirrv 
 |-  -. x e. x
45 elequ2 
 |-  ( x = y -> ( x e. x <-> x e. y ) )
46 44 45 mtbii 
 |-  ( x = y -> -. x e. y )
47 46 sps 
 |-  ( A. x x = y -> -. x e. y )
48 47 pm2.21d 
 |-  ( A. x x = y -> ( x e. y -> E. x ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) ) )
49 axregndlem1 
 |-  ( A. x x = z -> ( x e. y -> E. x ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) ) )
50 43 48 49 pm2.61ii 
 |-  ( x e. y -> E. x ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) )