This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sbequ2

Description: An equality theorem for substitution. (Contributed by NM, 16-May-1993) Revise df-sb . (Revised by BJ, 22-Dec-2020) (Proof shortened by Wolf Lammen, 3-Feb-2024)

Ref Expression
Assertion sbequ2 ( 𝑥 = 𝑡 → ( [ 𝑡 / 𝑥 ] 𝜑 → 𝜑 ) )

Proof

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 ⊢ ( 𝑥 = 𝑡 → ( [ 𝑡 / 𝑥 ] 𝜑 → 𝜑 ) )