Metamath Proof Explorer

Theorem wl-nfeqfb

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

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

Proof

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