# Metamath Proof Explorer

## Theorem ax13lem1

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}\to \left({z}={y}\to \forall {x}\phantom{\rule{.4em}{0ex}}{z}={y}\right)$

### Proof

Step Hyp Ref Expression
1 equvinva ${⊢}{z}={y}\to \exists {w}\phantom{\rule{.4em}{0ex}}\left({z}={w}\wedge {y}={w}\right)$
2 ax13v ${⊢}¬{x}={y}\to \left({y}={w}\to \forall {x}\phantom{\rule{.4em}{0ex}}{y}={w}\right)$
3 equeucl ${⊢}{z}={w}\to \left({y}={w}\to {z}={y}\right)$
4 3 alimdv ${⊢}{z}={w}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{y}={w}\to \forall {x}\phantom{\rule{.4em}{0ex}}{z}={y}\right)$
5 2 4 syl9 ${⊢}¬{x}={y}\to \left({z}={w}\to \left({y}={w}\to \forall {x}\phantom{\rule{.4em}{0ex}}{z}={y}\right)\right)$
6 5 impd ${⊢}¬{x}={y}\to \left(\left({z}={w}\wedge {y}={w}\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}{z}={y}\right)$
7 6 exlimdv ${⊢}¬{x}={y}\to \left(\exists {w}\phantom{\rule{.4em}{0ex}}\left({z}={w}\wedge {y}={w}\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}{z}={y}\right)$
8 1 7 syl5 ${⊢}¬{x}={y}\to \left({z}={y}\to \forall {x}\phantom{\rule{.4em}{0ex}}{z}={y}\right)$