Metamath Proof Explorer


Theorem sbft

Description: Substitution has no effect on a nonfree 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 ( Ⅎ 𝑥 𝜑 → ( [ 𝑦 / 𝑥 ] 𝜑𝜑 ) )