Description: Under the assumption -. x = y the reverse direction of 19.2 is provable from Tarski's FOL and ax13v only. Note that in conjunction with 19.2 in fact ( -. x = y -> ( A. x z = y <-> E. x z = y ) ) holds. (Contributed by Wolf Lammen, 17-Apr-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | wl-19.2reqv | |- ( -. x = y -> ( E. x z = y -> A. x z = y ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax13lem2 | |- ( -. x = y -> ( E. x z = y -> z = y ) ) |
|
| 2 | ax13lem1 | |- ( -. x = y -> ( z = y -> A. x z = y ) ) |
|
| 3 | 1 2 | syld | |- ( -. x = y -> ( E. x z = y -> A. x z = y ) ) |