Metamath Proof Explorer

Theorem axrepndlem2

Description: Lemma for the Axiom of Replacement with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 2-Jan-2002) (Proof shortened by Mario Carneiro, 6-Dec-2016) (New usage is discouraged.)

Ref Expression
Assertion axrepndlem2 
|- ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ -. A. y y = z ) -> E. x ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) )

Proof

Step Hyp Ref Expression
1 axrepndlem1 
 |-  ( -. A. y y = z -> E. w ( E. y A. z ( [ w / x ] ph -> z = y ) -> A. z ( z e. w <-> E. w ( w e. y /\ A. y [ w / x ] ph ) ) ) )
2 nfnae 
 |-  F/ x -. A. x x = y
3 nfnae 
 |-  F/ x -. A. x x = z
4 2 3 nfan 
 |-  F/ x ( -. A. x x = y /\ -. A. x x = z )
5 nfnae 
 |-  F/ y -. A. x x = y
6 nfnae 
 |-  F/ y -. A. x x = z
7 5 6 nfan 
 |-  F/ y ( -. A. x x = y /\ -. A. x x = z )
8 nfnae 
 |-  F/ z -. A. x x = y
9 nfnae 
 |-  F/ z -. A. x x = z
10 8 9 nfan 
 |-  F/ z ( -. A. x x = y /\ -. A. x x = z )
11 nfs1v 
 |-  F/ x [ w / x ] ph
12 11 a1i 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x [ w / x ] ph )
13 nfcvf 
 |-  ( -. A. x x = z -> F/_ x z )
14 13 adantl 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/_ x z )
15 nfcvf 
 |-  ( -. A. x x = y -> F/_ x y )
16 15 adantr 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/_ x y )
17 14 16 nfeqd 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x z = y )
18 12 17 nfimd 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x ( [ w / x ] ph -> z = y ) )
19 10 18 nfald 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x A. z ( [ w / x ] ph -> z = y ) )
20 7 19 nfexd 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x E. y A. z ( [ w / x ] ph -> z = y ) )
21 nfcvd 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/_ x w )
22 14 21 nfeld 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x z e. w )
23 nfv 
 |-  F/ w ( -. A. x x = y /\ -. A. x x = z )
24 21 16 nfeld 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x w e. y )
25 7 12 nfald 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x A. y [ w / x ] ph )
26 24 25 nfand 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x ( w e. y /\ A. y [ w / x ] ph ) )
27 23 26 nfexd 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x E. w ( w e. y /\ A. y [ w / x ] ph ) )
28 22 27 nfbid 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x ( z e. w <-> E. w ( w e. y /\ A. y [ w / x ] ph ) ) )
29 10 28 nfald 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x A. z ( z e. w <-> E. w ( w e. y /\ A. y [ w / x ] ph ) ) )
30 20 29 nfimd 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x ( E. y A. z ( [ w / x ] ph -> z = y ) -> A. z ( z e. w <-> E. w ( w e. y /\ A. y [ w / x ] ph ) ) ) )
31 nfcvd 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/_ y w )
32 nfcvf2 
 |-  ( -. A. x x = y -> F/_ y x )
33 32 adantr 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/_ y x )
34 31 33 nfeqd 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ y w = x )
35 7 34 nfan1 
 |-  F/ y ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x )
36 nfcvd 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/_ z w )
37 nfcvf2 
 |-  ( -. A. x x = z -> F/_ z x )
38 37 adantl 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/_ z x )
39 36 38 nfeqd 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ z w = x )
40 10 39 nfan1 
 |-  F/ z ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x )
41 sbequ12r 
 |-  ( w = x -> ( [ w / x ] ph <-> ph ) )
42 41 imbi1d 
 |-  ( w = x -> ( ( [ w / x ] ph -> z = y ) <-> ( ph -> z = y ) ) )
43 42 adantl 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( ( [ w / x ] ph -> z = y ) <-> ( ph -> z = y ) ) )
44 40 43 albid 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( A. z ( [ w / x ] ph -> z = y ) <-> A. z ( ph -> z = y ) ) )
45 35 44 exbid 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( E. y A. z ( [ w / x ] ph -> z = y ) <-> E. y A. z ( ph -> z = y ) ) )
46 elequ2 
 |-  ( w = x -> ( z e. w <-> z e. x ) )
47 46 adantl 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( z e. w <-> z e. x ) )
48 elequ1 
 |-  ( w = x -> ( w e. y <-> x e. y ) )
49 48 adantl 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( w e. y <-> x e. y ) )
50 41 adantl 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( [ w / x ] ph <-> ph ) )
51 35 50 albid 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( A. y [ w / x ] ph <-> A. y ph ) )
52 49 51 anbi12d 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( ( w e. y /\ A. y [ w / x ] ph ) <-> ( x e. y /\ A. y ph ) ) )
53 52 ex 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> ( w = x -> ( ( w e. y /\ A. y [ w / x ] ph ) <-> ( x e. y /\ A. y ph ) ) ) )
54 4 26 53 cbvexd 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> ( E. w ( w e. y /\ A. y [ w / x ] ph ) <-> E. x ( x e. y /\ A. y ph ) ) )
55 54 adantr 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( E. w ( w e. y /\ A. y [ w / x ] ph ) <-> E. x ( x e. y /\ A. y ph ) ) )
56 47 55 bibi12d 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( ( z e. w <-> E. w ( w e. y /\ A. y [ w / x ] ph ) ) <-> ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) )
57 40 56 albid 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( A. z ( z e. w <-> E. w ( w e. y /\ A. y [ w / x ] ph ) ) <-> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) )
58 45 57 imbi12d 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( ( E. y A. z ( [ w / x ] ph -> z = y ) -> A. z ( z e. w <-> E. w ( w e. y /\ A. y [ w / x ] ph ) ) ) <-> ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) ) )
59 58 ex 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> ( w = x -> ( ( E. y A. z ( [ w / x ] ph -> z = y ) -> A. z ( z e. w <-> E. w ( w e. y /\ A. y [ w / x ] ph ) ) ) <-> ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) ) ) )
60 4 30 59 cbvexd 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> ( E. w ( E. y A. z ( [ w / x ] ph -> z = y ) -> A. z ( z e. w <-> E. w ( w e. y /\ A. y [ w / x ] ph ) ) ) <-> E. x ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) ) )
61 1 60 imbitrid 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> ( -. A. y y = z -> E. x ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) ) )
62 61 imp 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ -. A. y y = z ) -> E. x ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) )