This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem equvel

Description: A variable elimination law for equality with no distinct variable requirements. Compare equvini . Usage of this theorem is discouraged because it depends on ax-13 . Use equvelv when possible. (Contributed by NM, 1-Mar-2013) (Proof shortened by Mario Carneiro, 17-Oct-2016) (Proof shortened by Wolf Lammen, 15-Jun-2019) (New usage is discouraged.)

Ref Expression
Assertion equvel ⊢ ∀ z z = x ↔ z = y → x = y

Proof

Step Hyp Ref Expression
1 albi ⊢ ∀ z z = x ↔ z = y → ∀ z z = x ↔ ∀ z z = y
2 ax6e ⊢ ∃ z z = y
3 biimpr ⊢ z = x ↔ z = y → z = y → z = x
4 ax7 ⊢ z = x → z = y → x = y
5 3 4 syli ⊢ z = x ↔ z = y → z = y → x = y
6 5 com12 ⊢ z = y → z = x ↔ z = y → x = y
7 2 6 eximii ⊢ ∃ z z = x ↔ z = y → x = y
8 7 19.35i ⊢ ∀ z z = x ↔ z = y → ∃ z x = y
9 4 spsd ⊢ z = x → ∀ z z = y → x = y
10 9 sps ⊢ ∀ z z = x → ∀ z z = y → x = y
11 10 a1dd ⊢ ∀ z z = x → ∀ z z = y → ∃ z x = y → x = y
12 nfeqf ⊢ ¬ ∀ z z = x ∧ ¬ ∀ z z = y → Ⅎ z x = y
13 12 19.9d ⊢ ¬ ∀ z z = x ∧ ¬ ∀ z z = y → ∃ z x = y → x = y
14 13 ex ⊢ ¬ ∀ z z = x → ¬ ∀ z z = y → ∃ z x = y → x = y
15 11 14 bija ⊢ ∀ z z = x ↔ ∀ z z = y → ∃ z x = y → x = y
16 1 8 15 sylc ⊢ ∀ z z = x ↔ z = y → x = y