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)

	Ref	Expression
Hypothesis	sbt.1	$$⊢\phi$$
Assertion	sbt	$$⊢\left[t/x\right]\phi$$

Proof

Step	Hyp	Ref	Expression
1		sbt.1	$$⊢\phi$$
2	1	a1i	$$⊢x=y\to \phi$$
3	2	ax-gen	$$⊢\forall x\left(x=y\to \phi \right)$$
4	3	a1i	$$⊢y=t\to \forall x\left(x=y\to \phi \right)$$
5	4	ax-gen	$$⊢\forall y\left(y=t\to \forall x\left(x=y\to \phi \right)\right)$$
6		df-sb	$$⊢\left[t/x\right]\phi \leftrightarrow \forall y\left(y=t\to \forall x\left(x=y\to \phi \right)\right)$$
7	5 6	mpbir	$$⊢\left[t/x\right]\phi$$