# Metamath Proof Explorer

## Theorem ax13

Description: Derive ax-13 from ax13v and Tarski's FOL. This shows that the weakening in ax13v is still sufficient for a complete system. Preferably, use the weaker ax13w to avoid the propagation of ax-13 . (Contributed by NM, 21-Dec-2015) (Proof shortened by Wolf Lammen, 31-Jan-2018) Reduce axiom usage (Revised by Wolf Lammen, 2-Jun-2021) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 equvinv ${⊢}{y}={z}↔\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}={y}\wedge {w}={z}\right)$
2 ax13lem1 ${⊢}¬{x}={y}\to \left({w}={y}\to \forall {x}\phantom{\rule{.4em}{0ex}}{w}={y}\right)$
3 2 imp ${⊢}\left(¬{x}={y}\wedge {w}={y}\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}{w}={y}$
4 ax13lem1 ${⊢}¬{x}={z}\to \left({w}={z}\to \forall {x}\phantom{\rule{.4em}{0ex}}{w}={z}\right)$
5 4 imp ${⊢}\left(¬{x}={z}\wedge {w}={z}\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}{w}={z}$
6 ax7v1 ${⊢}{w}={y}\to \left({w}={z}\to {y}={z}\right)$
7 6 imp ${⊢}\left({w}={y}\wedge {w}={z}\right)\to {y}={z}$
8 7 alanimi ${⊢}\left(\forall {x}\phantom{\rule{.4em}{0ex}}{w}={y}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}{w}={z}\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}{y}={z}$
9 3 5 8 syl2an ${⊢}\left(\left(¬{x}={y}\wedge {w}={y}\right)\wedge \left(¬{x}={z}\wedge {w}={z}\right)\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}{y}={z}$
10 9 an4s ${⊢}\left(\left(¬{x}={y}\wedge ¬{x}={z}\right)\wedge \left({w}={y}\wedge {w}={z}\right)\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}{y}={z}$
11 10 ex ${⊢}\left(¬{x}={y}\wedge ¬{x}={z}\right)\to \left(\left({w}={y}\wedge {w}={z}\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}{y}={z}\right)$
12 11 exlimdv ${⊢}\left(¬{x}={y}\wedge ¬{x}={z}\right)\to \left(\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}={y}\wedge {w}={z}\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}{y}={z}\right)$
13 1 12 syl5bi ${⊢}\left(¬{x}={y}\wedge ¬{x}={z}\right)\to \left({y}={z}\to \forall {x}\phantom{\rule{.4em}{0ex}}{y}={z}\right)$
14 13 ex ${⊢}¬{x}={y}\to \left(¬{x}={z}\to \left({y}={z}\to \forall {x}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\right)$
15 ax13b ${⊢}\left(¬{x}={y}\to \left({y}={z}\to \forall {x}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\right)↔\left(¬{x}={y}\to \left(¬{x}={z}\to \left({y}={z}\to \forall {x}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\right)\right)$
16 14 15 mpbir ${⊢}¬{x}={y}\to \left({y}={z}\to \forall {x}\phantom{\rule{.4em}{0ex}}{y}={z}\right)$