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 does not require ax-13 . (Contributed by NM, 12-Aug-1993) (Revised by Gino Giotto, 10-Jan-2024)

Ref Expression
Hypothesis hbsbw.1 φ z φ
Assertion hbsbw y x φ z y x φ


Step Hyp Ref Expression
1 hbsbw.1 φ z φ
2 1 nf5i z φ
3 2 nfsbv z y x φ
4 3 nf5ri y x φ z y x φ