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 ⊢¬∀zz=x∧¬∀zz=y→Ⅎzx=y

Proof

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