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 biimtrid ⊢ ¬ 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