Step 
Hyp 
Ref 
Expression 
1 

dfsb 
⊢ ( [ 𝑡 / 𝑥 ] 𝜑 ↔ ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) 
2 
1

biimpi 
⊢ ( [ 𝑡 / 𝑥 ] 𝜑 → ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) 
3 

equvinva 
⊢ ( 𝑥 = 𝑡 → ∃ 𝑦 ( 𝑥 = 𝑦 ∧ 𝑡 = 𝑦 ) ) 
4 

equcomi 
⊢ ( 𝑡 = 𝑦 → 𝑦 = 𝑡 ) 
5 

sp 
⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → ( 𝑥 = 𝑦 → 𝜑 ) ) 
6 
4 5

imim12i 
⊢ ( ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) → ( 𝑡 = 𝑦 → ( 𝑥 = 𝑦 → 𝜑 ) ) ) 
7 
6

impcomd 
⊢ ( ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) → ( ( 𝑥 = 𝑦 ∧ 𝑡 = 𝑦 ) → 𝜑 ) ) 
8 
7

aleximi 
⊢ ( ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) → ( ∃ 𝑦 ( 𝑥 = 𝑦 ∧ 𝑡 = 𝑦 ) → ∃ 𝑦 𝜑 ) ) 
9 
2 3 8

syl2im 
⊢ ( [ 𝑡 / 𝑥 ] 𝜑 → ( 𝑥 = 𝑡 → ∃ 𝑦 𝜑 ) ) 
10 

ax5e 
⊢ ( ∃ 𝑦 𝜑 → 𝜑 ) 
11 
9 10

syl6com 
⊢ ( 𝑥 = 𝑡 → ( [ 𝑡 / 𝑥 ] 𝜑 → 𝜑 ) ) 