Theorem hbsb

Description: If z is not free in ph , it is not free in [ y / x ] ph when y and z are distinct. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker hbsbw when possible. (Contributed by NM, 12-Aug-1993) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hbsb.1	$$⊢\phi \to \forall z\phi$$
Assertion	hbsb	$$⊢\left[y/x\right]\phi \to \forall z\left[y/x\right]\phi$$

Proof

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