Step |
Hyp |
Ref |
Expression |
1 |
|
vex |
|- x e. _V |
2 |
|
vex |
|- y e. _V |
3 |
1 2
|
eqvinop |
|- ( A = <. x , y >. <-> E. z E. w ( A = <. z , w >. /\ <. z , w >. = <. x , y >. ) ) |
4 |
|
19.8a |
|- ( E. y ( <. z , w >. = <. x , y >. /\ ph ) -> E. x E. y ( <. z , w >. = <. x , y >. /\ ph ) ) |
5 |
4
|
19.23bi |
|- ( ( <. z , w >. = <. x , y >. /\ ph ) -> E. x E. y ( <. z , w >. = <. x , y >. /\ ph ) ) |
6 |
5
|
ex |
|- ( <. z , w >. = <. x , y >. -> ( ph -> E. x E. y ( <. z , w >. = <. x , y >. /\ ph ) ) ) |
7 |
|
vex |
|- z e. _V |
8 |
|
vex |
|- w e. _V |
9 |
7 8
|
opth |
|- ( <. z , w >. = <. x , y >. <-> ( z = x /\ w = y ) ) |
10 |
9
|
anbi1i |
|- ( ( <. z , w >. = <. x , y >. /\ ph ) <-> ( ( z = x /\ w = y ) /\ ph ) ) |
11 |
10
|
2exbii |
|- ( E. x E. y ( <. z , w >. = <. x , y >. /\ ph ) <-> E. x E. y ( ( z = x /\ w = y ) /\ ph ) ) |
12 |
|
nfe1 |
|- F/ x E. x ( z = x /\ E. y ( w = y /\ ph ) ) |
13 |
|
19.8a |
|- ( ( w = y /\ ph ) -> E. y ( w = y /\ ph ) ) |
14 |
13
|
anim2i |
|- ( ( z = x /\ ( w = y /\ ph ) ) -> ( z = x /\ E. y ( w = y /\ ph ) ) ) |
15 |
14
|
anassrs |
|- ( ( ( z = x /\ w = y ) /\ ph ) -> ( z = x /\ E. y ( w = y /\ ph ) ) ) |
16 |
15
|
eximi |
|- ( E. y ( ( z = x /\ w = y ) /\ ph ) -> E. y ( z = x /\ E. y ( w = y /\ ph ) ) ) |
17 |
|
biidd |
|- ( A. y y = x -> ( ( z = x /\ E. y ( w = y /\ ph ) ) <-> ( z = x /\ E. y ( w = y /\ ph ) ) ) ) |
18 |
17
|
drex1 |
|- ( A. y y = x -> ( E. y ( z = x /\ E. y ( w = y /\ ph ) ) <-> E. x ( z = x /\ E. y ( w = y /\ ph ) ) ) ) |
19 |
16 18
|
syl5ib |
|- ( A. y y = x -> ( E. y ( ( z = x /\ w = y ) /\ ph ) -> E. x ( z = x /\ E. y ( w = y /\ ph ) ) ) ) |
20 |
|
anass |
|- ( ( ( z = x /\ w = y ) /\ ph ) <-> ( z = x /\ ( w = y /\ ph ) ) ) |
21 |
20
|
exbii |
|- ( E. y ( ( z = x /\ w = y ) /\ ph ) <-> E. y ( z = x /\ ( w = y /\ ph ) ) ) |
22 |
|
19.40 |
|- ( E. y ( z = x /\ ( w = y /\ ph ) ) -> ( E. y z = x /\ E. y ( w = y /\ ph ) ) ) |
23 |
|
nfeqf2 |
|- ( -. A. y y = x -> F/ y z = x ) |
24 |
23
|
19.9d |
|- ( -. A. y y = x -> ( E. y z = x -> z = x ) ) |
25 |
24
|
anim1d |
|- ( -. A. y y = x -> ( ( E. y z = x /\ E. y ( w = y /\ ph ) ) -> ( z = x /\ E. y ( w = y /\ ph ) ) ) ) |
26 |
22 25
|
syl5 |
|- ( -. A. y y = x -> ( E. y ( z = x /\ ( w = y /\ ph ) ) -> ( z = x /\ E. y ( w = y /\ ph ) ) ) ) |
27 |
21 26
|
syl5bi |
|- ( -. A. y y = x -> ( E. y ( ( z = x /\ w = y ) /\ ph ) -> ( z = x /\ E. y ( w = y /\ ph ) ) ) ) |
28 |
|
19.8a |
|- ( ( z = x /\ E. y ( w = y /\ ph ) ) -> E. x ( z = x /\ E. y ( w = y /\ ph ) ) ) |
29 |
27 28
|
syl6 |
|- ( -. A. y y = x -> ( E. y ( ( z = x /\ w = y ) /\ ph ) -> E. x ( z = x /\ E. y ( w = y /\ ph ) ) ) ) |
30 |
19 29
|
pm2.61i |
|- ( E. y ( ( z = x /\ w = y ) /\ ph ) -> E. x ( z = x /\ E. y ( w = y /\ ph ) ) ) |
31 |
12 30
|
exlimi |
|- ( E. x E. y ( ( z = x /\ w = y ) /\ ph ) -> E. x ( z = x /\ E. y ( w = y /\ ph ) ) ) |
32 |
|
euequ |
|- E! x x = z |
33 |
|
equcom |
|- ( x = z <-> z = x ) |
34 |
33
|
eubii |
|- ( E! x x = z <-> E! x z = x ) |
35 |
32 34
|
mpbi |
|- E! x z = x |
36 |
|
eupick |
|- ( ( E! x z = x /\ E. x ( z = x /\ E. y ( w = y /\ ph ) ) ) -> ( z = x -> E. y ( w = y /\ ph ) ) ) |
37 |
35 36
|
mpan |
|- ( E. x ( z = x /\ E. y ( w = y /\ ph ) ) -> ( z = x -> E. y ( w = y /\ ph ) ) ) |
38 |
37
|
com12 |
|- ( z = x -> ( E. x ( z = x /\ E. y ( w = y /\ ph ) ) -> E. y ( w = y /\ ph ) ) ) |
39 |
|
euequ |
|- E! y y = w |
40 |
|
equcom |
|- ( y = w <-> w = y ) |
41 |
40
|
eubii |
|- ( E! y y = w <-> E! y w = y ) |
42 |
39 41
|
mpbi |
|- E! y w = y |
43 |
|
eupick |
|- ( ( E! y w = y /\ E. y ( w = y /\ ph ) ) -> ( w = y -> ph ) ) |
44 |
42 43
|
mpan |
|- ( E. y ( w = y /\ ph ) -> ( w = y -> ph ) ) |
45 |
44
|
com12 |
|- ( w = y -> ( E. y ( w = y /\ ph ) -> ph ) ) |
46 |
38 45
|
sylan9 |
|- ( ( z = x /\ w = y ) -> ( E. x ( z = x /\ E. y ( w = y /\ ph ) ) -> ph ) ) |
47 |
31 46
|
syl5 |
|- ( ( z = x /\ w = y ) -> ( E. x E. y ( ( z = x /\ w = y ) /\ ph ) -> ph ) ) |
48 |
11 47
|
syl5bi |
|- ( ( z = x /\ w = y ) -> ( E. x E. y ( <. z , w >. = <. x , y >. /\ ph ) -> ph ) ) |
49 |
9 48
|
sylbi |
|- ( <. z , w >. = <. x , y >. -> ( E. x E. y ( <. z , w >. = <. x , y >. /\ ph ) -> ph ) ) |
50 |
6 49
|
impbid |
|- ( <. z , w >. = <. x , y >. -> ( ph <-> E. x E. y ( <. z , w >. = <. x , y >. /\ ph ) ) ) |
51 |
|
eqeq1 |
|- ( A = <. z , w >. -> ( A = <. x , y >. <-> <. z , w >. = <. x , y >. ) ) |
52 |
51
|
anbi1d |
|- ( A = <. z , w >. -> ( ( A = <. x , y >. /\ ph ) <-> ( <. z , w >. = <. x , y >. /\ ph ) ) ) |
53 |
52
|
2exbidv |
|- ( A = <. z , w >. -> ( E. x E. y ( A = <. x , y >. /\ ph ) <-> E. x E. y ( <. z , w >. = <. x , y >. /\ ph ) ) ) |
54 |
53
|
bibi2d |
|- ( A = <. z , w >. -> ( ( ph <-> E. x E. y ( A = <. x , y >. /\ ph ) ) <-> ( ph <-> E. x E. y ( <. z , w >. = <. x , y >. /\ ph ) ) ) ) |
55 |
51 54
|
imbi12d |
|- ( A = <. z , w >. -> ( ( A = <. x , y >. -> ( ph <-> E. x E. y ( A = <. x , y >. /\ ph ) ) ) <-> ( <. z , w >. = <. x , y >. -> ( ph <-> E. x E. y ( <. z , w >. = <. x , y >. /\ ph ) ) ) ) ) |
56 |
50 55
|
mpbiri |
|- ( A = <. z , w >. -> ( A = <. x , y >. -> ( ph <-> E. x E. y ( A = <. x , y >. /\ ph ) ) ) ) |
57 |
56
|
adantr |
|- ( ( A = <. z , w >. /\ <. z , w >. = <. x , y >. ) -> ( A = <. x , y >. -> ( ph <-> E. x E. y ( A = <. x , y >. /\ ph ) ) ) ) |
58 |
57
|
exlimivv |
|- ( E. z E. w ( A = <. z , w >. /\ <. z , w >. = <. x , y >. ) -> ( A = <. x , y >. -> ( ph <-> E. x E. y ( A = <. x , y >. /\ ph ) ) ) ) |
59 |
3 58
|
sylbi |
|- ( A = <. x , y >. -> ( A = <. x , y >. -> ( ph <-> E. x E. y ( A = <. x , y >. /\ ph ) ) ) ) |
60 |
59
|
pm2.43i |
|- ( A = <. x , y >. -> ( ph <-> E. x E. y ( A = <. x , y >. /\ ph ) ) ) |