Theorem sbft

Description: Substitution has no effect on a non-free variable. (Contributed by NM, 30-May-2009) (Revised by Mario Carneiro, 12-Oct-2016) (Proof shortened by Wolf Lammen, 3-May-2018)

	Ref	Expression
Assertion	sbft	⊢ ( Ⅎ 𝑥 𝜑 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		spsbe	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 → ∃ 𝑥 𝜑 )
2		19.9t	⊢ ( Ⅎ 𝑥 𝜑 → ( ∃ 𝑥 𝜑 ↔ 𝜑 ) )
3	1 2	syl5ib	⊢ ( Ⅎ 𝑥 𝜑 → ( [ 𝑦 / 𝑥 ] 𝜑 → 𝜑 ) )
4		nf5r	⊢ ( Ⅎ 𝑥 𝜑 → ( 𝜑 → ∀ 𝑥 𝜑 ) )
5		stdpc4	⊢ ( ∀ 𝑥 𝜑 → [ 𝑦 / 𝑥 ] 𝜑 )
6	4 5	syl6	⊢ ( Ⅎ 𝑥 𝜑 → ( 𝜑 → [ 𝑦 / 𝑥 ] 𝜑 ) )
7	3 6	impbid	⊢ ( Ⅎ 𝑥 𝜑 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜑 ) )