Metamath Proof Explorer

Theorem wl-sb8ft

Description: Substitution of variable in universal quantifier. Closed form of sb8f . (Contributed by Wolf Lammen, 27-Apr-2025)

Ref Expression
Assertion wl-sb8ft ⊢ ∀ x Ⅎ y φ → ∀ x φ ↔ ∀ y y x φ

Proof

Step Hyp Ref Expression
1 sbft ⊢ Ⅎ y φ → x y φ ↔ φ
2 1 alimi ⊢ ∀ x Ⅎ y φ → ∀ x x y φ ↔ φ
3 albi ⊢ ∀ x x y φ ↔ φ → ∀ x x y φ ↔ ∀ x φ
4 2 3 syl ⊢ ∀ x Ⅎ y φ → ∀ x x y φ ↔ ∀ x φ
5 wl-sb9v ⊢ ∀ x x y φ ↔ ∀ y y x φ
6 4 5 bitr3di ⊢ ∀ x Ⅎ y φ → ∀ x φ ↔ ∀ y y x φ