Step |
Hyp |
Ref |
Expression |
1 |
|
nfeqf |
|- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x y = z ) |
2 |
1
|
ex |
|- ( -. A. x x = y -> ( -. A. x x = z -> F/ x y = z ) ) |
3 |
|
sbft |
|- ( F/ x y = z -> ( [ y / x ] y = z <-> y = z ) ) |
4 |
2 3
|
syl6com |
|- ( -. A. x x = z -> ( -. A. x x = y -> ( [ y / x ] y = z <-> y = z ) ) ) |
5 |
|
sbequ12r |
|- ( y = x -> ( [ y / x ] y = z <-> y = z ) ) |
6 |
5
|
equcoms |
|- ( x = y -> ( [ y / x ] y = z <-> y = z ) ) |
7 |
6
|
sps |
|- ( A. x x = y -> ( [ y / x ] y = z <-> y = z ) ) |
8 |
4 7
|
pm2.61d2 |
|- ( -. A. x x = z -> ( [ y / x ] y = z <-> y = z ) ) |