Metamath Proof Explorer

Theorem wl-sbalnae

Description: A theorem used in elimination of disjoint variable restrictions by replacing them with distinctors. (Contributed by Wolf Lammen, 25-Jul-2019)

Ref Expression
Assertion wl-sbalnae ⊢¬∀xx=y∧¬∀xx=z→zy∀xφ↔∀xzyφ

Proof

Step Hyp Ref Expression
1 sb4b ⊢¬∀yy=z→zy∀xφ↔∀yy=z→∀xφ
2 nfnae ⊢Ⅎy¬∀xx=y
3 nfnae ⊢Ⅎy¬∀xx=z
4 2 3 nfan ⊢Ⅎy¬∀xx=y∧¬∀xx=z
5 nfeqf ⊢¬∀xx=y∧¬∀xx=z→Ⅎxy=z
6 19.21t ⊢Ⅎxy=z→∀xy=z→φ↔y=z→∀xφ
7 6 bicomd ⊢Ⅎxy=z→y=z→∀xφ↔∀xy=z→φ
8 5 7 syl ⊢¬∀xx=y∧¬∀xx=z→y=z→∀xφ↔∀xy=z→φ
9 4 8 albid ⊢¬∀xx=y∧¬∀xx=z→∀yy=z→∀xφ↔∀y∀xy=z→φ
10 1 9 sylan9bbr ⊢¬∀xx=y∧¬∀xx=z∧¬∀yy=z→zy∀xφ↔∀y∀xy=z→φ
11 nfnae ⊢Ⅎx¬∀yy=z
12 sb4b ⊢¬∀yy=z→zyφ↔∀yy=z→φ
13 11 12 albid ⊢¬∀yy=z→∀xzyφ↔∀x∀yy=z→φ
14 alcom ⊢∀x∀yy=z→φ↔∀y∀xy=z→φ
15 13 14 bitrdi ⊢¬∀yy=z→∀xzyφ↔∀y∀xy=z→φ
16 15 adantl ⊢¬∀xx=y∧¬∀xx=z∧¬∀yy=z→∀xzyφ↔∀y∀xy=z→φ
17 10 16 bitr4d ⊢¬∀xx=y∧¬∀xx=z∧¬∀yy=z→zy∀xφ↔∀xzyφ
18 17 ex ⊢¬∀xx=y∧¬∀xx=z→¬∀yy=z→zy∀xφ↔∀xzyφ
19 sbequ12 ⊢y=z→∀xφ↔zy∀xφ
20 19 sps ⊢∀yy=z→∀xφ↔zy∀xφ
21 sbequ12 ⊢y=z→φ↔zyφ
22 21 sps ⊢∀yy=z→φ↔zyφ
23 22 dral2 ⊢∀yy=z→∀xφ↔∀xzyφ
24 20 23 bitr3d ⊢∀yy=z→zy∀xφ↔∀xzyφ
25 18 24 pm2.61d2 ⊢¬∀xx=y∧¬∀xx=z→zy∀xφ↔∀xzyφ