Theorem bj-sbf4

Description: Substitution has no effect on a bound variable (nonfreeness case); see sbf2 . (Contributed by BJ, 2-May-2019)

	Ref	Expression
Assertion	bj-sbf4	⊢ ( [ 𝑦 / 𝑥 ] Ⅎ 𝑥 𝜑 ↔ Ⅎ 𝑥 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		nfnf1	⊢ Ⅎ 𝑥 Ⅎ 𝑥 𝜑
2	1	sbf	⊢ ( [ 𝑦 / 𝑥 ] Ⅎ 𝑥 𝜑 ↔ Ⅎ 𝑥 𝜑 )