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

Metamath Proof Explorer

Theorem nfeqf

Description: A variable is effectively not free in an equality if it is not either of the involved variables. F/ version of ax-c9 . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Mario Carneiro, 6-Oct-2016) Remove dependency on ax-11 . (Revised by Wolf Lammen, 6-Sep-2018) (New usage is discouraged.)

Ref Expression
Assertion nfeqf ⊢ ¬ ∀ z z = x ∧ ¬ ∀ z z = y → Ⅎ z x = y

Proof

Step Hyp Ref Expression
1 nfna1 ⊢ Ⅎ z ¬ ∀ z z = x
2 nfna1 ⊢ Ⅎ z ¬ ∀ z z = y
3 1 2 nfan ⊢ Ⅎ z ¬ ∀ z z = x ∧ ¬ ∀ z z = y
4 equvinva ⊢ x = y → ∃ w x = w ∧ y = w
5 dveeq1 ⊢ ¬ ∀ z z = x → x = w → ∀ z x = w
6 5 imp ⊢ ¬ ∀ z z = x ∧ x = w → ∀ z x = w
7 dveeq1 ⊢ ¬ ∀ z z = y → y = w → ∀ z y = w
8 7 imp ⊢ ¬ ∀ z z = y ∧ y = w → ∀ z y = w
9 equtr2 ⊢ x = w ∧ y = w → x = y
10 9 alanimi ⊢ ∀ z x = w ∧ ∀ z y = w → ∀ z x = y
11 6 8 10 syl2an ⊢ ¬ ∀ z z = x ∧ x = w ∧ ¬ ∀ z z = y ∧ y = w → ∀ z x = y
12 11 an4s ⊢ ¬ ∀ z z = x ∧ ¬ ∀ z z = y ∧ x = w ∧ y = w → ∀ z x = y
13 12 ex ⊢ ¬ ∀ z z = x ∧ ¬ ∀ z z = y → x = w ∧ y = w → ∀ z x = y
14 13 exlimdv ⊢ ¬ ∀ z z = x ∧ ¬ ∀ z z = y → ∃ w x = w ∧ y = w → ∀ z x = y
15 4 14 syl5 ⊢ ¬ ∀ z z = x ∧ ¬ ∀ z z = y → x = y → ∀ z x = y
16 3 15 nf5d ⊢ ¬ ∀ z z = x ∧ ¬ ∀ z z = y → Ⅎ z x = y