Metamath Proof Explorer

Theorem sbal2

Description: Move quantifier in and out of substitution. (Contributed by NM, 2-Jan-2002) Remove a distinct variable constraint. (Revised by Wolf Lammen, 24-Dec-2022) (Proof shortened by Wolf Lammen, 23-Sep-2023) Usage of this theorem is discouraged because it depends on ax-13 . Use sbal instead. (New usage is discouraged.)

Ref Expression
Assertion sbal2 ⊢¬∀xx=y→zy∀xφ↔∀xzyφ

Proof

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