Metamath Proof Explorer

Theorem sbal1

Description: Check out sbal for a version not dependent on ax-13 . A theorem used in elimination of disjoint variable restriction on x and z by replacing it with a distinctor -. A. x x = z . (Contributed by NM, 15-May-1993) (Proof shortened by Wolf Lammen, 3-Oct-2018) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion sbal1 ⊢¬∀xx=z→zy∀xφ↔∀xzyφ

Proof

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