Description: Under the assumption -. x = y a specialized version of 19.8a is provable from Tarski's FOL and ax13v only. Note that this reverts the implication in ax13lem2 , so in fact ( -. x = y -> ( E. x z = y <-> z = y ) ) holds. (Contributed by Wolf Lammen, 17-Apr-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | wl-19.8eqv | |- ( -. x = y -> ( z = y -> E. x z = y ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax13lem1 | |- ( -. x = y -> ( z = y -> A. x z = y ) ) |
|
2 | 19.2 | |- ( A. x z = y -> E. x z = y ) |
|
3 | 1 2 | syl6 | |- ( -. x = y -> ( z = y -> E. x z = y ) ) |