# Metamath Proof Explorer

## Theorem ax13lem2

Description: Lemma for nfeqf2 . This lemma is equivalent to ax13v with one distinct variable constraint removed. (Contributed by Wolf Lammen, 8-Sep-2018) Reduce axiom usage. (Revised by Wolf Lammen, 18-Oct-2020) (New usage is discouraged.)

Ref Expression
Assertion ax13lem2 ${⊢}¬{x}={y}\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{z}={y}\to {z}={y}\right)$

### Proof

Step Hyp Ref Expression
1 ax13lem1 ${⊢}¬{x}={y}\to \left({w}={y}\to \forall {x}\phantom{\rule{.4em}{0ex}}{w}={y}\right)$
2 equeucl ${⊢}{z}={y}\to \left({w}={y}\to {z}={w}\right)$
3 2 eximi ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{z}={y}\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({w}={y}\to {z}={w}\right)$
4 19.36v ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({w}={y}\to {z}={w}\right)↔\left(\forall {x}\phantom{\rule{.4em}{0ex}}{w}={y}\to {z}={w}\right)$
5 3 4 sylib ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{z}={y}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{w}={y}\to {z}={w}\right)$
6 1 5 syl9 ${⊢}¬{x}={y}\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{z}={y}\to \left({w}={y}\to {z}={w}\right)\right)$
7 6 alrimdv ${⊢}¬{x}={y}\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{z}={y}\to \forall {w}\phantom{\rule{.4em}{0ex}}\left({w}={y}\to {z}={w}\right)\right)$
8 equequ2 ${⊢}{w}={y}\to \left({z}={w}↔{z}={y}\right)$
9 8 equsalvw ${⊢}\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}={y}\to {z}={w}\right)↔{z}={y}$
10 7 9 syl6ib ${⊢}¬{x}={y}\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{z}={y}\to {z}={y}\right)$