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	$$⊢\phi \to \forall z\phi$$
Assertion	hbsbw	$$⊢\left[y/x\right]\phi \to \forall z\left[y/x\right]\phi$$

Proof

Step	Hyp	Ref	Expression
1		hbsbw.1	$$⊢\phi \to \forall z\phi$$
2	1	nf5i	$$⊢Ⅎz\phi$$
3	2	nfsbv	$$⊢Ⅎz\left[y/x\right]\phi$$
4	3	nf5ri	$$⊢\left[y/x\right]\phi \to \forall z\left[y/x\right]\phi$$