Step |
Hyp |
Ref |
Expression |
1 |
|
sp |
|- ( A. x x = y -> x = y ) |
2 |
|
p0ex |
|- { (/) } e. _V |
3 |
|
eleq2 |
|- ( x = { (/) } -> ( w e. x <-> w e. { (/) } ) ) |
4 |
3
|
imbi2d |
|- ( x = { (/) } -> ( ( w = (/) -> w e. x ) <-> ( w = (/) -> w e. { (/) } ) ) ) |
5 |
4
|
albidv |
|- ( x = { (/) } -> ( A. w ( w = (/) -> w e. x ) <-> A. w ( w = (/) -> w e. { (/) } ) ) ) |
6 |
2 5
|
spcev |
|- ( A. w ( w = (/) -> w e. { (/) } ) -> E. x A. w ( w = (/) -> w e. x ) ) |
7 |
|
0ex |
|- (/) e. _V |
8 |
7
|
snid |
|- (/) e. { (/) } |
9 |
|
eleq1 |
|- ( w = (/) -> ( w e. { (/) } <-> (/) e. { (/) } ) ) |
10 |
8 9
|
mpbiri |
|- ( w = (/) -> w e. { (/) } ) |
11 |
6 10
|
mpg |
|- E. x A. w ( w = (/) -> w e. x ) |
12 |
|
neq0 |
|- ( -. w = (/) <-> E. x x e. w ) |
13 |
12
|
con1bii |
|- ( -. E. x x e. w <-> w = (/) ) |
14 |
13
|
imbi1i |
|- ( ( -. E. x x e. w -> w e. x ) <-> ( w = (/) -> w e. x ) ) |
15 |
14
|
albii |
|- ( A. w ( -. E. x x e. w -> w e. x ) <-> A. w ( w = (/) -> w e. x ) ) |
16 |
15
|
exbii |
|- ( E. x A. w ( -. E. x x e. w -> w e. x ) <-> E. x A. w ( w = (/) -> w e. x ) ) |
17 |
11 16
|
mpbir |
|- E. x A. w ( -. E. x x e. w -> w e. x ) |
18 |
|
nfnae |
|- F/ x -. A. x x = y |
19 |
|
nfnae |
|- F/ y -. A. x x = y |
20 |
|
nfcvf2 |
|- ( -. A. x x = y -> F/_ y x ) |
21 |
|
nfcvd |
|- ( -. A. x x = y -> F/_ y w ) |
22 |
20 21
|
nfeld |
|- ( -. A. x x = y -> F/ y x e. w ) |
23 |
18 22
|
nfexd |
|- ( -. A. x x = y -> F/ y E. x x e. w ) |
24 |
23
|
nfnd |
|- ( -. A. x x = y -> F/ y -. E. x x e. w ) |
25 |
21 20
|
nfeld |
|- ( -. A. x x = y -> F/ y w e. x ) |
26 |
24 25
|
nfimd |
|- ( -. A. x x = y -> F/ y ( -. E. x x e. w -> w e. x ) ) |
27 |
|
nfeqf2 |
|- ( -. A. x x = y -> F/ x w = y ) |
28 |
18 27
|
nfan1 |
|- F/ x ( -. A. x x = y /\ w = y ) |
29 |
|
elequ2 |
|- ( w = y -> ( x e. w <-> x e. y ) ) |
30 |
29
|
adantl |
|- ( ( -. A. x x = y /\ w = y ) -> ( x e. w <-> x e. y ) ) |
31 |
28 30
|
exbid |
|- ( ( -. A. x x = y /\ w = y ) -> ( E. x x e. w <-> E. x x e. y ) ) |
32 |
31
|
notbid |
|- ( ( -. A. x x = y /\ w = y ) -> ( -. E. x x e. w <-> -. E. x x e. y ) ) |
33 |
|
elequ1 |
|- ( w = y -> ( w e. x <-> y e. x ) ) |
34 |
33
|
adantl |
|- ( ( -. A. x x = y /\ w = y ) -> ( w e. x <-> y e. x ) ) |
35 |
32 34
|
imbi12d |
|- ( ( -. A. x x = y /\ w = y ) -> ( ( -. E. x x e. w -> w e. x ) <-> ( -. E. x x e. y -> y e. x ) ) ) |
36 |
35
|
ex |
|- ( -. A. x x = y -> ( w = y -> ( ( -. E. x x e. w -> w e. x ) <-> ( -. E. x x e. y -> y e. x ) ) ) ) |
37 |
19 26 36
|
cbvald |
|- ( -. A. x x = y -> ( A. w ( -. E. x x e. w -> w e. x ) <-> A. y ( -. E. x x e. y -> y e. x ) ) ) |
38 |
18 37
|
exbid |
|- ( -. A. x x = y -> ( E. x A. w ( -. E. x x e. w -> w e. x ) <-> E. x A. y ( -. E. x x e. y -> y e. x ) ) ) |
39 |
17 38
|
mpbii |
|- ( -. A. x x = y -> E. x A. y ( -. E. x x e. y -> y e. x ) ) |
40 |
|
nfae |
|- F/ x A. x x = z |
41 |
|
nfae |
|- F/ y A. x x = z |
42 |
|
axc11r |
|- ( A. x x = z -> ( A. z -. x e. y -> A. x -. x e. y ) ) |
43 |
|
alnex |
|- ( A. z -. x e. y <-> -. E. z x e. y ) |
44 |
|
alnex |
|- ( A. x -. x e. y <-> -. E. x x e. y ) |
45 |
42 43 44
|
3imtr3g |
|- ( A. x x = z -> ( -. E. z x e. y -> -. E. x x e. y ) ) |
46 |
|
nd3 |
|- ( A. x x = z -> -. A. y x e. z ) |
47 |
46
|
pm2.21d |
|- ( A. x x = z -> ( A. y x e. z -> -. E. x x e. y ) ) |
48 |
45 47
|
jad |
|- ( A. x x = z -> ( ( E. z x e. y -> A. y x e. z ) -> -. E. x x e. y ) ) |
49 |
48
|
spsd |
|- ( A. x x = z -> ( A. x ( E. z x e. y -> A. y x e. z ) -> -. E. x x e. y ) ) |
50 |
49
|
imim1d |
|- ( A. x x = z -> ( ( -. E. x x e. y -> y e. x ) -> ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) ) |
51 |
41 50
|
alimd |
|- ( A. x x = z -> ( A. y ( -. E. x x e. y -> y e. x ) -> A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) ) |
52 |
40 51
|
eximd |
|- ( A. x x = z -> ( E. x A. y ( -. E. x x e. y -> y e. x ) -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) ) |
53 |
39 52
|
syl5com |
|- ( -. A. x x = y -> ( A. x x = z -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) ) |
54 |
|
axpowndlem2 |
|- ( -. A. x x = y -> ( -. A. x x = z -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) ) |
55 |
53 54
|
pm2.61d |
|- ( -. A. x x = y -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) |
56 |
1 55
|
nsyl5 |
|- ( -. x = y -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) |