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 ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ) → Ⅎ 𝑧 𝑥 = 𝑦 )

Proof

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