Metamath Proof Explorer

Theorem axrepnd

Description: A version of 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) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 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 ) ) ) )
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/ x -. A. y y = z
6 4 5 nfan 
 |-  F/ x ( ( -. A. x x = y /\ -. A. x x = z ) /\ -. A. y y = z )
7 nfnae 
 |-  F/ z -. A. x x = y
8 nfnae 
 |-  F/ z -. A. x x = z
9 7 8 nfan 
 |-  F/ z ( -. A. x x = y /\ -. A. x x = z )
10 nfnae 
 |-  F/ z -. A. y y = z
11 9 10 nfan 
 |-  F/ z ( ( -. A. x x = y /\ -. A. x x = z ) /\ -. A. y y = z )
12 nfcvf 
 |-  ( -. A. y y = z -> F/_ y z )
13 12 adantl 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ -. A. y y = z ) -> F/_ y z )
14 nfcvf2 
 |-  ( -. A. x x = y -> F/_ y x )
15 14 ad2antrr 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ -. A. y y = z ) -> F/_ y x )
16 13 15 nfeld 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ -. A. y y = z ) -> F/ y z e. x )
17 16 nf5rd 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ -. A. y y = z ) -> ( z e. x -> A. y z e. x ) )
18 sp 
 |-  ( A. y z e. x -> z e. x )
19 17 18 impbid1 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ -. A. y y = z ) -> ( z e. x <-> A. y z e. x ) )
20 nfcvf2 
 |-  ( -. A. x x = z -> F/_ z x )
21 20 ad2antlr 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ -. A. y y = z ) -> F/_ z x )
22 nfcvf2 
 |-  ( -. A. y y = z -> F/_ z y )
23 22 adantl 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ -. A. y y = z ) -> F/_ z y )
24 21 23 nfeld 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ -. A. y y = z ) -> F/ z x e. y )
25 24 nf5rd 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ -. A. y y = z ) -> ( x e. y -> A. z x e. y ) )
26 sp 
 |-  ( A. z x e. y -> x e. y )
27 25 26 impbid1 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ -. A. y y = z ) -> ( x e. y <-> A. z x e. y ) )
28 27 anbi1d 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ -. A. y y = z ) -> ( ( x e. y /\ A. y ph ) <-> ( A. z x e. y /\ A. y ph ) ) )
29 6 28 exbid 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ -. A. y y = z ) -> ( E. x ( x e. y /\ A. y ph ) <-> E. x ( A. z x e. y /\ A. y ph ) ) )
30 19 29 bibi12d 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ -. A. y y = z ) -> ( ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) <-> ( A. y z e. x <-> E. x ( A. z x e. y /\ A. y ph ) ) ) )
31 11 30 albid 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ -. A. y y = z ) -> ( A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) <-> A. z ( A. y z e. x <-> E. x ( A. z x e. y /\ A. y ph ) ) ) )
32 31 imbi2d 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ -. A. y y = z ) -> ( ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) <-> ( E. y A. z ( ph -> z = y ) -> A. z ( A. y z e. x <-> E. x ( A. z x e. y /\ A. y ph ) ) ) ) )
33 6 32 exbid 
 |-  ( ( ( -. 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 ) ) ) <-> E. x ( E. y A. z ( ph -> z = y ) -> A. z ( A. y z e. x <-> E. x ( A. z x e. y /\ A. y ph ) ) ) ) )
34 1 33 mpbid 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ -. A. y y = z ) -> E. x ( E. y A. z ( ph -> z = y ) -> A. z ( A. y z e. x <-> E. x ( A. z x e. y /\ A. y ph ) ) ) )
35 34 exp31 
 |-  ( -. A. x x = y -> ( -. A. x x = z -> ( -. A. y y = z -> E. x ( E. y A. z ( ph -> z = y ) -> A. z ( A. y z e. x <-> E. x ( A. z x e. y /\ A. y ph ) ) ) ) ) )
36 nfae 
 |-  F/ z A. x x = y
37 nd2 
 |-  ( A. y y = x -> -. A. y z e. x )
38 37 aecoms 
 |-  ( A. x x = y -> -. A. y z e. x )
39 nfae 
 |-  F/ x A. x x = y
40 nd3 
 |-  ( A. x x = y -> -. A. z x e. y )
41 40 intnanrd 
 |-  ( A. x x = y -> -. ( A. z x e. y /\ A. y ph ) )
42 39 41 nexd 
 |-  ( A. x x = y -> -. E. x ( A. z x e. y /\ A. y ph ) )
43 38 42 2falsed 
 |-  ( A. x x = y -> ( A. y z e. x <-> E. x ( A. z x e. y /\ A. y ph ) ) )
44 36 43 alrimi 
 |-  ( A. x x = y -> A. z ( A. y z e. x <-> E. x ( A. z x e. y /\ A. y ph ) ) )
45 44 a1d 
 |-  ( A. x x = y -> ( E. y A. z ( ph -> z = y ) -> A. z ( A. y z e. x <-> E. x ( A. z x e. y /\ A. y ph ) ) ) )
46 45 19.8ad 
 |-  ( A. x x = y -> E. x ( E. y A. z ( ph -> z = y ) -> A. z ( A. y z e. x <-> E. x ( A. z x e. y /\ A. y ph ) ) ) )
47 nfae 
 |-  F/ z A. x x = z
48 nd4 
 |-  ( A. x x = z -> -. A. y z e. x )
49 nfae 
 |-  F/ x A. x x = z
50 nd1 
 |-  ( A. z z = x -> -. A. z x e. y )
51 50 aecoms 
 |-  ( A. x x = z -> -. A. z x e. y )
52 51 intnanrd 
 |-  ( A. x x = z -> -. ( A. z x e. y /\ A. y ph ) )
53 49 52 nexd 
 |-  ( A. x x = z -> -. E. x ( A. z x e. y /\ A. y ph ) )
54 48 53 2falsed 
 |-  ( A. x x = z -> ( A. y z e. x <-> E. x ( A. z x e. y /\ A. y ph ) ) )
55 47 54 alrimi 
 |-  ( A. x x = z -> A. z ( A. y z e. x <-> E. x ( A. z x e. y /\ A. y ph ) ) )
56 55 a1d 
 |-  ( A. x x = z -> ( E. y A. z ( ph -> z = y ) -> A. z ( A. y z e. x <-> E. x ( A. z x e. y /\ A. y ph ) ) ) )
57 56 19.8ad 
 |-  ( A. x x = z -> E. x ( E. y A. z ( ph -> z = y ) -> A. z ( A. y z e. x <-> E. x ( A. z x e. y /\ A. y ph ) ) ) )
58 nfae 
 |-  F/ z A. y y = z
59 nd1 
 |-  ( A. y y = z -> -. A. y z e. x )
60 nfae 
 |-  F/ x A. y y = z
61 nd2 
 |-  ( A. z z = y -> -. A. z x e. y )
62 61 aecoms 
 |-  ( A. y y = z -> -. A. z x e. y )
63 62 intnanrd 
 |-  ( A. y y = z -> -. ( A. z x e. y /\ A. y ph ) )
64 60 63 nexd 
 |-  ( A. y y = z -> -. E. x ( A. z x e. y /\ A. y ph ) )
65 59 64 2falsed 
 |-  ( A. y y = z -> ( A. y z e. x <-> E. x ( A. z x e. y /\ A. y ph ) ) )
66 58 65 alrimi 
 |-  ( A. y y = z -> A. z ( A. y z e. x <-> E. x ( A. z x e. y /\ A. y ph ) ) )
67 66 a1d 
 |-  ( A. y y = z -> ( E. y A. z ( ph -> z = y ) -> A. z ( A. y z e. x <-> E. x ( A. z x e. y /\ A. y ph ) ) ) )
68 67 19.8ad 
 |-  ( A. y y = z -> E. x ( E. y A. z ( ph -> z = y ) -> A. z ( A. y z e. x <-> E. x ( A. z x e. y /\ A. y ph ) ) ) )
69 35 46 57 68 pm2.61iii 
 |-  E. x ( E. y A. z ( ph -> z = y ) -> A. z ( A. y z e. x <-> E. x ( A. z x e. y /\ A. y ph ) ) )