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

Metamath Proof Explorer

Theorem sbt

Description: A substitution into a theorem yields a theorem. See sbtALT for a shorter proof requiring more axioms. See chvar and chvarv for versions using implicit substitution. (Contributed by NM, 21-Jan-2004) (Proof shortened by Andrew Salmon, 25-May-2011) (Proof shortened by Wolf Lammen, 20-Jul-2018) Revise df-sb . (Revised by Steven Nguyen, 6-Jul-2023) Revise df-sb again. (Revised by Wolf Lammen, 4-Feb-2026)

Ref Expression
Hypothesis sbt.1 ⊢ 𝜑
Assertion sbt [ 𝑡 / 𝑥 ] 𝜑

Proof

Step Hyp Ref Expression
1 sbt.1 ⊢ 𝜑
2 1 sbtlem ⊢ ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
3 1 sbtlem ⊢ ∀ 𝑧 ( 𝑧 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) )
4 2 3 2th ⊢ ( ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ↔ ∀ 𝑧 ( 𝑧 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) )
5 4 df-sb ⊢ ( [ 𝑡 / 𝑥 ] 𝜑 ↔ ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
6 2 5 mpbir ⊢ [ 𝑡 / 𝑥 ] 𝜑