Step |
Hyp |
Ref |
Expression |
1 |
|
axpowndlem3 |
|- ( -. x = w -> E. x A. w ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) ) |
2 |
1
|
ax-gen |
|- A. w ( -. x = w -> E. x A. w ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) ) |
3 |
|
nfnae |
|- F/ y -. A. y y = x |
4 |
|
nfnae |
|- F/ y -. A. y y = z |
5 |
3 4
|
nfan |
|- F/ y ( -. A. y y = x /\ -. A. y y = z ) |
6 |
|
nfcvf |
|- ( -. A. y y = x -> F/_ y x ) |
7 |
6
|
adantr |
|- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ y x ) |
8 |
|
nfcvd |
|- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ y w ) |
9 |
7 8
|
nfeqd |
|- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y x = w ) |
10 |
9
|
nfnd |
|- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y -. x = w ) |
11 |
|
nfnae |
|- F/ x -. A. y y = x |
12 |
|
nfnae |
|- F/ x -. A. y y = z |
13 |
11 12
|
nfan |
|- F/ x ( -. A. y y = x /\ -. A. y y = z ) |
14 |
|
nfv |
|- F/ w ( -. A. y y = x /\ -. A. y y = z ) |
15 |
|
nfnae |
|- F/ z -. A. y y = x |
16 |
|
nfnae |
|- F/ z -. A. y y = z |
17 |
15 16
|
nfan |
|- F/ z ( -. A. y y = x /\ -. A. y y = z ) |
18 |
7 8
|
nfeld |
|- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y x e. w ) |
19 |
17 18
|
nfexd |
|- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y E. z x e. w ) |
20 |
|
nfcvf |
|- ( -. A. y y = z -> F/_ y z ) |
21 |
20
|
adantl |
|- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ y z ) |
22 |
7 21
|
nfeld |
|- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y x e. z ) |
23 |
14 22
|
nfald |
|- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y A. w x e. z ) |
24 |
19 23
|
nfimd |
|- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y ( E. z x e. w -> A. w x e. z ) ) |
25 |
13 24
|
nfald |
|- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y A. x ( E. z x e. w -> A. w x e. z ) ) |
26 |
8 7
|
nfeld |
|- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y w e. x ) |
27 |
25 26
|
nfimd |
|- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) ) |
28 |
14 27
|
nfald |
|- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y A. w ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) ) |
29 |
13 28
|
nfexd |
|- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y E. x A. w ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) ) |
30 |
10 29
|
nfimd |
|- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y ( -. x = w -> E. x A. w ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) ) ) |
31 |
|
equequ2 |
|- ( w = y -> ( x = w <-> x = y ) ) |
32 |
31
|
notbid |
|- ( w = y -> ( -. x = w <-> -. x = y ) ) |
33 |
32
|
adantl |
|- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( -. x = w <-> -. x = y ) ) |
34 |
|
nfcvd |
|- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ x w ) |
35 |
|
nfcvf2 |
|- ( -. A. y y = x -> F/_ x y ) |
36 |
35
|
adantr |
|- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ x y ) |
37 |
34 36
|
nfeqd |
|- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ x w = y ) |
38 |
13 37
|
nfan1 |
|- F/ x ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) |
39 |
|
nfcvd |
|- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ z w ) |
40 |
|
nfcvf2 |
|- ( -. A. y y = z -> F/_ z y ) |
41 |
40
|
adantl |
|- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ z y ) |
42 |
39 41
|
nfeqd |
|- ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ z w = y ) |
43 |
17 42
|
nfan1 |
|- F/ z ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) |
44 |
|
elequ2 |
|- ( w = y -> ( x e. w <-> x e. y ) ) |
45 |
44
|
adantl |
|- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( x e. w <-> x e. y ) ) |
46 |
43 45
|
exbid |
|- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( E. z x e. w <-> E. z x e. y ) ) |
47 |
|
biidd |
|- ( w = y -> ( x e. z <-> x e. z ) ) |
48 |
47
|
a1i |
|- ( ( -. A. y y = x /\ -. A. y y = z ) -> ( w = y -> ( x e. z <-> x e. z ) ) ) |
49 |
5 22 48
|
cbvald |
|- ( ( -. A. y y = x /\ -. A. y y = z ) -> ( A. w x e. z <-> A. y x e. z ) ) |
50 |
49
|
adantr |
|- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( A. w x e. z <-> A. y x e. z ) ) |
51 |
46 50
|
imbi12d |
|- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( ( E. z x e. w -> A. w x e. z ) <-> ( E. z x e. y -> A. y x e. z ) ) ) |
52 |
38 51
|
albid |
|- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( A. x ( E. z x e. w -> A. w x e. z ) <-> A. x ( E. z x e. y -> A. y x e. z ) ) ) |
53 |
|
elequ1 |
|- ( w = y -> ( w e. x <-> y e. x ) ) |
54 |
53
|
adantl |
|- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( w e. x <-> y e. x ) ) |
55 |
52 54
|
imbi12d |
|- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) <-> ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) ) |
56 |
55
|
ex |
|- ( ( -. A. y y = x /\ -. A. y y = z ) -> ( w = y -> ( ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) <-> ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) ) ) |
57 |
5 27 56
|
cbvald |
|- ( ( -. A. y y = x /\ -. A. y y = z ) -> ( A. w ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) <-> A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) ) |
58 |
13 57
|
exbid |
|- ( ( -. A. y y = x /\ -. A. y y = z ) -> ( E. x A. w ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) <-> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) ) |
59 |
58
|
adantr |
|- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( E. x A. w ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) <-> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) ) |
60 |
33 59
|
imbi12d |
|- ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( ( -. x = w -> E. x A. w ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) ) <-> ( -. x = y -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) ) ) |
61 |
60
|
ex |
|- ( ( -. A. y y = x /\ -. A. y y = z ) -> ( w = y -> ( ( -. x = w -> E. x A. w ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) ) <-> ( -. x = y -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) ) ) ) |
62 |
5 30 61
|
cbvald |
|- ( ( -. A. y y = x /\ -. A. y y = z ) -> ( A. w ( -. x = w -> E. x A. w ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) ) <-> A. y ( -. x = y -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) ) ) |
63 |
2 62
|
mpbii |
|- ( ( -. A. y y = x /\ -. A. y y = z ) -> A. y ( -. x = y -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) ) |
64 |
63
|
19.21bi |
|- ( ( -. A. y y = x /\ -. A. y y = z ) -> ( -. x = y -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) ) |
65 |
64
|
ex |
|- ( -. A. y y = x -> ( -. A. y y = z -> ( -. x = y -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) ) ) |