Theorem sbv

Description: Substitution for a variable not occurring in a proposition. See sbf for a version without disjoint variable condition on x , ph . If one adds a disjoint variable condition on x , t , then sbv can be proved directly by chaining equsv with sb6 . (Contributed by BJ, 22-Dec-2020)

	Ref	Expression
Assertion	sbv	$$⊢\left[t/x\right]\phi \leftrightarrow \phi$$

Proof

Step	Hyp	Ref	Expression
1		spsbe	$$⊢\left[t/x\right]\phi \to \exists x\phi$$
2		ax5e	$$⊢\exists x\phi \to \phi$$
3	1 2	syl	$$⊢\left[t/x\right]\phi \to \phi$$
4		ax-5	$$⊢\phi \to \forall x\phi$$
5		stdpc4	$$⊢\forall x\phi \to \left[t/x\right]\phi$$
6	4 5	syl	$$⊢\phi \to \left[t/x\right]\phi$$
7	3 6	impbii	$$⊢\left[t/x\right]\phi \leftrightarrow \phi$$