Metamath Proof Explorer

Theorem hbsbw

Description: If z is not free in ph , it is not free in [ y / x ] ph when y and z are distinct. Version of hbsb with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 12-Aug-1993) (Revised by Gino Giotto, 23-May-2024)

Ref Expression
Hypothesis hbsbw.1 ⊢ φ → ∀ z φ
Assertion hbsbw ⊢ y x φ → ∀ z y x φ

Proof

Step Hyp Ref Expression
1 hbsbw.1 ⊢ φ → ∀ z φ
2 df-sb ⊢ y x φ ↔ ∀ w w = y → ∀ x x = w → φ
3 1 imim2i ⊢ x = w → φ → x = w → ∀ z φ
4 3 alimi ⊢ ∀ x x = w → φ → ∀ x x = w → ∀ z φ
5 19.21v ⊢ ∀ z x = w → φ ↔ x = w → ∀ z φ
6 5 biimpri ⊢ x = w → ∀ z φ → ∀ z x = w → φ
7 6 alimi ⊢ ∀ x x = w → ∀ z φ → ∀ x ∀ z x = w → φ
8 ax-11 ⊢ ∀ x ∀ z x = w → φ → ∀ z ∀ x x = w → φ
9 4 7 8 3syl ⊢ ∀ x x = w → φ → ∀ z ∀ x x = w → φ
10 9 imim2i ⊢ w = y → ∀ x x = w → φ → w = y → ∀ z ∀ x x = w → φ
11 19.21v ⊢ ∀ z w = y → ∀ x x = w → φ ↔ w = y → ∀ z ∀ x x = w → φ
12 10 11 sylibr ⊢ w = y → ∀ x x = w → φ → ∀ z w = y → ∀ x x = w → φ
13 12 hbal ⊢ ∀ w w = y → ∀ x x = w → φ → ∀ z ∀ w w = y → ∀ x x = w → φ
14 2 13 hbxfrbi ⊢ y x φ → ∀ z y x φ