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	⊢ [ 𝑡 / 𝑥 ] 𝜑