Metamath Proof Explorer

Theorem wl-nfeqfb

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

Ref Expression
Assertion wl-nfeqfb ⊢ Ⅎ x y = z ↔ ∀ x x = y ↔ ∀ x x = z

Proof

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