Description: A version of ax13v with one distinct variable restriction dropped. For convenience, y is kept on the right side of equations. The proof of ax13 bases on ideas from NM, 24-Dec-2015. (Contributed by Wolf Lammen, 8-Sep-2018) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ax13lem1 | |- ( -. x = y -> ( z = y -> A. x z = y ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | equvinva | |- ( z = y -> E. w ( z = w /\ y = w ) ) |
|
| 2 | ax13v | |- ( -. x = y -> ( y = w -> A. x y = w ) ) |
|
| 3 | equeucl | |- ( z = w -> ( y = w -> z = y ) ) |
|
| 4 | 3 | alimdv | |- ( z = w -> ( A. x y = w -> A. x z = y ) ) |
| 5 | 2 4 | syl9 | |- ( -. x = y -> ( z = w -> ( y = w -> A. x z = y ) ) ) |
| 6 | 5 | impd | |- ( -. x = y -> ( ( z = w /\ y = w ) -> A. x z = y ) ) |
| 7 | 6 | exlimdv | |- ( -. x = y -> ( E. w ( z = w /\ y = w ) -> A. x z = y ) ) |
| 8 | 1 7 | syl5 | |- ( -. x = y -> ( z = y -> A. x z = y ) ) |