This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ z y ∀ x φ ↔ ∀ x z y φ

Proof

Step Hyp Ref Expression
1 alcom ⊢ ∀ w ∀ x w = z → ∀ y y = w → φ ↔ ∀ x ∀ w w = z → ∀ y y = w → φ
2 19.21v ⊢ ∀ x y = w → φ ↔ y = w → ∀ x φ
3 2 albii ⊢ ∀ y ∀ x y = w → φ ↔ ∀ y y = w → ∀ x φ
4 alcom ⊢ ∀ y ∀ x y = w → φ ↔ ∀ x ∀ y y = w → φ
5 3 4 bitr3i ⊢ ∀ y y = w → ∀ x φ ↔ ∀ x ∀ y y = w → φ
6 5 imbi2i ⊢ w = z → ∀ y y = w → ∀ x φ ↔ w = z → ∀ x ∀ y y = w → φ
7 6 albii ⊢ ∀ w w = z → ∀ y y = w → ∀ x φ ↔ ∀ w w = z → ∀ x ∀ y y = w → φ
8 dfsb ⊢ z y ∀ x φ ↔ ∀ w w = z → ∀ y y = w → ∀ x φ
9 19.21v ⊢ ∀ x w = z → ∀ y y = w → φ ↔ w = z → ∀ x ∀ y y = w → φ
10 9 albii ⊢ ∀ w ∀ x w = z → ∀ y y = w → φ ↔ ∀ w w = z → ∀ x ∀ y y = w → φ
11 7 8 10 3bitr4i ⊢ z y ∀ x φ ↔ ∀ w ∀ x w = z → ∀ y y = w → φ
12 dfsb ⊢ z y φ ↔ ∀ w w = z → ∀ y y = w → φ
13 12 albii ⊢ ∀ x z y φ ↔ ∀ x ∀ w w = z → ∀ y y = w → φ
14 1 11 13 3bitr4i ⊢ z y ∀ x φ ↔ ∀ x z y φ