Theorem sbf

Description: Substitution for a variable not free in a wff does not affect it. For a version requiring disjoint variables but fewer axioms, see sbv . (Contributed by NM, 14-May-1993) (Revised by Mario Carneiro, 4-Oct-2016)

	Ref	Expression
Hypothesis	sbf.1	$$⊢Ⅎx\phi$$
Assertion	sbf	$$⊢\left[y/x\right]\phi \leftrightarrow \phi$$

Proof

Step	Hyp	Ref	Expression
1		sbf.1	$$⊢Ⅎx\phi$$
2		sbft	$$⊢Ⅎx\phi \to \left(\left[y/x\right]\phi \leftrightarrow \phi \right)$$
3	1 2	ax-mp	$$⊢\left[y/x\right]\phi \leftrightarrow \phi$$