Step |
Hyp |
Ref |
Expression |
1 |
|
dtru |
|- -. A. y y = z |
2 |
|
exnal |
|- ( E. y -. y = z <-> -. A. y y = z ) |
3 |
1 2
|
mpbir |
|- E. y -. y = z |
4 |
|
nfe1 |
|- F/ y E. y A. z ( A. y ( E. x y e. z -> A. z y e. x ) -> z e. y ) |
5 |
|
axpownd |
|- ( -. y = z -> E. y A. z ( A. y ( E. x y e. z -> A. z y e. x ) -> z e. y ) ) |
6 |
4 5
|
exlimi |
|- ( E. y -. y = z -> E. y A. z ( A. y ( E. x y e. z -> A. z y e. x ) -> z e. y ) ) |
7 |
3 6
|
ax-mp |
|- E. y A. z ( A. y ( E. x y e. z -> A. z y e. x ) -> z e. y ) |
8 |
|
19.9v |
|- ( E. x y e. z <-> y e. z ) |
9 |
|
19.3v |
|- ( A. z y e. x <-> y e. x ) |
10 |
8 9
|
imbi12i |
|- ( ( E. x y e. z -> A. z y e. x ) <-> ( y e. z -> y e. x ) ) |
11 |
10
|
albii |
|- ( A. y ( E. x y e. z -> A. z y e. x ) <-> A. y ( y e. z -> y e. x ) ) |
12 |
11
|
imbi1i |
|- ( ( A. y ( E. x y e. z -> A. z y e. x ) -> z e. y ) <-> ( A. y ( y e. z -> y e. x ) -> z e. y ) ) |
13 |
12
|
albii |
|- ( A. z ( A. y ( E. x y e. z -> A. z y e. x ) -> z e. y ) <-> A. z ( A. y ( y e. z -> y e. x ) -> z e. y ) ) |
14 |
13
|
exbii |
|- ( E. y A. z ( A. y ( E. x y e. z -> A. z y e. x ) -> z e. y ) <-> E. y A. z ( A. y ( y e. z -> y e. x ) -> z e. y ) ) |
15 |
7 14
|
mpbi |
|- E. y A. z ( A. y ( y e. z -> y e. x ) -> z e. y ) |
16 |
|
elequ1 |
|- ( w = y -> ( w e. z <-> y e. z ) ) |
17 |
|
elequ1 |
|- ( w = y -> ( w e. x <-> y e. x ) ) |
18 |
16 17
|
imbi12d |
|- ( w = y -> ( ( w e. z -> w e. x ) <-> ( y e. z -> y e. x ) ) ) |
19 |
18
|
cbvalvw |
|- ( A. w ( w e. z -> w e. x ) <-> A. y ( y e. z -> y e. x ) ) |
20 |
19
|
imbi1i |
|- ( ( A. w ( w e. z -> w e. x ) -> z e. y ) <-> ( A. y ( y e. z -> y e. x ) -> z e. y ) ) |
21 |
20
|
albii |
|- ( A. z ( A. w ( w e. z -> w e. x ) -> z e. y ) <-> A. z ( A. y ( y e. z -> y e. x ) -> z e. y ) ) |
22 |
21
|
exbii |
|- ( E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y ) <-> E. y A. z ( A. y ( y e. z -> y e. x ) -> z e. y ) ) |
23 |
15 22
|
mpbir |
|- E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y ) |