Theorem sbft

Description: Substitution has no effect on a non-free variable. (Contributed by NM, 30-May-2009) (Revised by Mario Carneiro, 12-Oct-2016) (Proof shortened by Wolf Lammen, 3-May-2018)

	Ref	Expression
Assertion	sbft	$$⊢Ⅎx\phi \to \left(\left[y/x\right]\phi \leftrightarrow \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		spsbe	$$⊢\left[y/x\right]\phi \to \exists x\phi$$
2		19.9t	$$⊢Ⅎx\phi \to \left(\exists x\phi \leftrightarrow \phi \right)$$
3	1 2	syl5ib	$$⊢Ⅎx\phi \to \left(\left[y/x\right]\phi \to \phi \right)$$
4		nf5r	$$⊢Ⅎx\phi \to \left(\phi \to \forall x\phi \right)$$
5		stdpc4	$$⊢\forall x\phi \to \left[y/x\right]\phi$$
6	4 5	syl6	$$⊢Ⅎx\phi \to \left(\phi \to \left[y/x\right]\phi \right)$$
7	3 6	impbid	$$⊢Ⅎx\phi \to \left(\left[y/x\right]\phi \leftrightarrow \phi \right)$$