Metamath Proof Explorer

Theorem sbal

Description: Move universal quantifier in and out of substitution. (Contributed by NM, 16-May-1993) (Proof shortened by Wolf Lammen, 29-Sep-2018) Reduce dependencies on axioms. (Revised by Steven Nguyen, 13-Aug-2023)

Ref Expression
Assertion sbal ⊢zy∀xφ↔∀xzyφ

Proof

Step Hyp Ref Expression
1 alcom ⊢∀w∀xw=z→∀yy=w→φ↔∀x∀ww=z→∀yy=w→φ
2 19.21v ⊢∀xy=w→φ↔y=w→∀xφ
3 2 albii ⊢∀y∀xy=w→φ↔∀yy=w→∀xφ
4 alcom ⊢∀y∀xy=w→φ↔∀x∀yy=w→φ
5 3 4 bitr3i ⊢∀yy=w→∀xφ↔∀x∀yy=w→φ
6 5 imbi2i ⊢w=z→∀yy=w→∀xφ↔w=z→∀x∀yy=w→φ
7 6 albii ⊢∀ww=z→∀yy=w→∀xφ↔∀ww=z→∀x∀yy=w→φ
8 df-sb ⊢zy∀xφ↔∀ww=z→∀yy=w→∀xφ
9 19.21v ⊢∀xw=z→∀yy=w→φ↔w=z→∀x∀yy=w→φ
10 9 albii ⊢∀w∀xw=z→∀yy=w→φ↔∀ww=z→∀x∀yy=w→φ
11 7 8 10 3bitr4i ⊢zy∀xφ↔∀w∀xw=z→∀yy=w→φ
12 df-sb ⊢zyφ↔∀ww=z→∀yy=w→φ
13 12 albii ⊢∀xzyφ↔∀x∀ww=z→∀yy=w→φ
14 1 11 13 3bitr4i ⊢zy∀xφ↔∀xzyφ