Step |
Hyp |
Ref |
Expression |
1 |
|
ax6e |
|- E. z z = x |
2 |
|
nfnae |
|- F/ z -. A. w w = z |
3 |
|
nfnae |
|- F/ z -. A. w w = x |
4 |
2 3
|
nfan |
|- F/ z ( -. A. w w = z /\ -. A. w w = x ) |
5 |
|
nfeqf |
|- ( ( -. A. w w = z /\ -. A. w w = x ) -> F/ w z = x ) |
6 |
|
pm3.21 |
|- ( w = y -> ( z = x -> ( z = x /\ w = y ) ) ) |
7 |
5 6
|
spimed |
|- ( ( -. A. w w = z /\ -. A. w w = x ) -> ( z = x -> E. w ( z = x /\ w = y ) ) ) |
8 |
4 7
|
eximd |
|- ( ( -. A. w w = z /\ -. A. w w = x ) -> ( E. z z = x -> E. z E. w ( z = x /\ w = y ) ) ) |
9 |
1 8
|
mpi |
|- ( ( -. A. w w = z /\ -. A. w w = x ) -> E. z E. w ( z = x /\ w = y ) ) |
10 |
9
|
ex |
|- ( -. A. w w = z -> ( -. A. w w = x -> E. z E. w ( z = x /\ w = y ) ) ) |
11 |
|
ax6e |
|- E. z z = y |
12 |
|
nfae |
|- F/ z A. w w = x |
13 |
|
equvini |
|- ( z = y -> E. w ( z = w /\ w = y ) ) |
14 |
|
equtrr |
|- ( w = x -> ( z = w -> z = x ) ) |
15 |
14
|
anim1d |
|- ( w = x -> ( ( z = w /\ w = y ) -> ( z = x /\ w = y ) ) ) |
16 |
15
|
aleximi |
|- ( A. w w = x -> ( E. w ( z = w /\ w = y ) -> E. w ( z = x /\ w = y ) ) ) |
17 |
13 16
|
syl5 |
|- ( A. w w = x -> ( z = y -> E. w ( z = x /\ w = y ) ) ) |
18 |
12 17
|
eximd |
|- ( A. w w = x -> ( E. z z = y -> E. z E. w ( z = x /\ w = y ) ) ) |
19 |
11 18
|
mpi |
|- ( A. w w = x -> E. z E. w ( z = x /\ w = y ) ) |
20 |
10 19
|
pm2.61d2 |
|- ( -. A. w w = z -> E. z E. w ( z = x /\ w = y ) ) |