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