Step |
Hyp |
Ref |
Expression |
1 |
|
equtr |
|- ( z = x -> ( x = y -> z = y ) ) |
2 |
|
equeuclr |
|- ( z = y -> ( x = y -> x = z ) ) |
3 |
2
|
anc2ri |
|- ( z = y -> ( x = y -> ( x = z /\ z = y ) ) ) |
4 |
1 3
|
syli |
|- ( z = x -> ( x = y -> ( x = z /\ z = y ) ) ) |
5 |
|
19.8a |
|- ( ( x = z /\ z = y ) -> E. z ( x = z /\ z = y ) ) |
6 |
4 5
|
syl6 |
|- ( z = x -> ( x = y -> E. z ( x = z /\ z = y ) ) ) |
7 |
|
ax13 |
|- ( -. z = x -> ( x = y -> A. z x = y ) ) |
8 |
|
ax6e |
|- E. z z = y |
9 |
8 3
|
eximii |
|- E. z ( x = y -> ( x = z /\ z = y ) ) |
10 |
9
|
19.35i |
|- ( A. z x = y -> E. z ( x = z /\ z = y ) ) |
11 |
7 10
|
syl6 |
|- ( -. z = x -> ( x = y -> E. z ( x = z /\ z = y ) ) ) |
12 |
6 11
|
pm2.61i |
|- ( x = y -> E. z ( x = z /\ z = y ) ) |