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	⊢ ( 𝜑 → ∀ 𝑧 𝜑 )
Assertion	hbsb	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 → ∀ 𝑧 [ 𝑦 / 𝑥 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		hbsb.1	⊢ ( 𝜑 → ∀ 𝑧 𝜑 )
2	1	nf5i	⊢ Ⅎ 𝑧 𝜑
3	2	nfsb	⊢ Ⅎ 𝑧 [ 𝑦 / 𝑥 ] 𝜑
4	3	nf5ri	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 → ∀ 𝑧 [ 𝑦 / 𝑥 ] 𝜑 )