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→y=z→∀xy=z

Proof

Step Hyp Ref Expression
1 equvinv ⊢y=z↔∃ww=y∧w=z
2 ax13lem1 ⊢¬x=y→w=y→∀xw=y
3 2 imp ⊢¬x=y∧w=y→∀xw=y
4 ax13lem1 ⊢¬x=z→w=z→∀xw=z
5 4 imp ⊢¬x=z∧w=z→∀xw=z
6 ax7v1 ⊢w=y→w=z→y=z
7 6 imp ⊢w=y∧w=z→y=z
8 7 alanimi ⊢∀xw=y∧∀xw=z→∀xy=z
9 3 5 8 syl2an ⊢¬x=y∧w=y∧¬x=z∧w=z→∀xy=z
10 9 an4s ⊢¬x=y∧¬x=z∧w=y∧w=z→∀xy=z
11 10 ex ⊢¬x=y∧¬x=z→w=y∧w=z→∀xy=z
12 11 exlimdv ⊢¬x=y∧¬x=z→∃ww=y∧w=z→∀xy=z
13 1 12 syl5bi ⊢¬x=y∧¬x=z→y=z→∀xy=z
14 13 ex ⊢¬x=y→¬x=z→y=z→∀xy=z
15 ax13b ⊢¬x=y→y=z→∀xy=z↔¬x=y→¬x=z→y=z→∀xy=z
16 14 15 mpbir ⊢¬x=y→y=z→∀xy=z