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 x y = z

Proof

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