Theorem wl-nfeqfb

Description: Extend nfeqf to an equivalence. (Contributed by Wolf Lammen, 31-Jul-2019)

	Ref	Expression
Assertion	wl-nfeqfb	⊢ ( Ⅎ 𝑥 𝑦 = 𝑧 ↔ ( ∀ 𝑥 𝑥 = 𝑦 ↔ ∀ 𝑥 𝑥 = 𝑧 ) )

Proof

Step	Hyp	Ref	Expression
1		nf5r	⊢ ( Ⅎ 𝑥 𝑦 = 𝑧 → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) )
2	1	imp	⊢ ( ( Ⅎ 𝑥 𝑦 = 𝑧 ∧ 𝑦 = 𝑧 ) → ∀ 𝑥 𝑦 = 𝑧 )
3		wl-aleq	⊢ ( ∀ 𝑥 𝑦 = 𝑧 ↔ ( 𝑦 = 𝑧 ∧ ( ∀ 𝑥 𝑥 = 𝑦 ↔ ∀ 𝑥 𝑥 = 𝑧 ) ) )
4	3	simprbi	⊢ ( ∀ 𝑥 𝑦 = 𝑧 → ( ∀ 𝑥 𝑥 = 𝑦 ↔ ∀ 𝑥 𝑥 = 𝑧 ) )
5	2 4	syl	⊢ ( ( Ⅎ 𝑥 𝑦 = 𝑧 ∧ 𝑦 = 𝑧 ) → ( ∀ 𝑥 𝑥 = 𝑦 ↔ ∀ 𝑥 𝑥 = 𝑧 ) )
6		nfnt	⊢ ( Ⅎ 𝑥 𝑦 = 𝑧 → Ⅎ 𝑥 ¬ 𝑦 = 𝑧 )
7	6	nf5rd	⊢ ( Ⅎ 𝑥 𝑦 = 𝑧 → ( ¬ 𝑦 = 𝑧 → ∀ 𝑥 ¬ 𝑦 = 𝑧 ) )
8	7	imp	⊢ ( ( Ⅎ 𝑥 𝑦 = 𝑧 ∧ ¬ 𝑦 = 𝑧 ) → ∀ 𝑥 ¬ 𝑦 = 𝑧 )
9		alnex	⊢ ( ∀ 𝑥 ¬ 𝑦 = 𝑧 ↔ ¬ ∃ 𝑥 𝑦 = 𝑧 )
10		wl-exeq	⊢ ( ∃ 𝑥 𝑦 = 𝑧 ↔ ( 𝑦 = 𝑧 ∨ ∀ 𝑥 𝑥 = 𝑦 ∨ ∀ 𝑥 𝑥 = 𝑧 ) )
11	9 10	xchbinx	⊢ ( ∀ 𝑥 ¬ 𝑦 = 𝑧 ↔ ¬ ( 𝑦 = 𝑧 ∨ ∀ 𝑥 𝑥 = 𝑦 ∨ ∀ 𝑥 𝑥 = 𝑧 ) )
12		3ioran	⊢ ( ¬ ( 𝑦 = 𝑧 ∨ ∀ 𝑥 𝑥 = 𝑦 ∨ ∀ 𝑥 𝑥 = 𝑧 ) ↔ ( ¬ 𝑦 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) )
13	11 12	sylbb	⊢ ( ∀ 𝑥 ¬ 𝑦 = 𝑧 → ( ¬ 𝑦 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) )
14		3simpc	⊢ ( ( ¬ 𝑦 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) )
15		pm5.21	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → ( ∀ 𝑥 𝑥 = 𝑦 ↔ ∀ 𝑥 𝑥 = 𝑧 ) )
16	8 13 14 15	4syl	⊢ ( ( Ⅎ 𝑥 𝑦 = 𝑧 ∧ ¬ 𝑦 = 𝑧 ) → ( ∀ 𝑥 𝑥 = 𝑦 ↔ ∀ 𝑥 𝑥 = 𝑧 ) )
17	5 16	pm2.61dan	⊢ ( Ⅎ 𝑥 𝑦 = 𝑧 → ( ∀ 𝑥 𝑥 = 𝑦 ↔ ∀ 𝑥 𝑥 = 𝑧 ) )
18		ax7	⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑧 → 𝑦 = 𝑧 ) )
19	18	al2imi	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 𝑥 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) )
20		nftht	⊢ ( ∀ 𝑥 𝑦 = 𝑧 → Ⅎ 𝑥 𝑦 = 𝑧 )
21	19 20	syl6	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 𝑥 = 𝑧 → Ⅎ 𝑥 𝑦 = 𝑧 ) )
22		nfeqf	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 𝑦 = 𝑧 )
23	22	ex	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ¬ ∀ 𝑥 𝑥 = 𝑧 → Ⅎ 𝑥 𝑦 = 𝑧 ) )
24	21 23	bija	⊢ ( ( ∀ 𝑥 𝑥 = 𝑦 ↔ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 𝑦 = 𝑧 )
25	17 24	impbii	⊢ ( Ⅎ 𝑥 𝑦 = 𝑧 ↔ ( ∀ 𝑥 𝑥 = 𝑦 ↔ ∀ 𝑥 𝑥 = 𝑧 ) )