Theorem sbctt

Description: Substitution for a variable not free in a wff does not affect it. (Contributed by Mario Carneiro, 14-Oct-2016)

	Ref	Expression
Assertion	sbctt	$$⊢\left(A\in V\wedge Ⅎx\phi \right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		dfsbcq2	$$⊢y=A\to \left(\left[y/x\right]\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
2	1	bibi1d	$$⊢y=A\to \left(\left(\left[y/x\right]\phi \leftrightarrow \phi \right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \phi \right)\right)$$
3	2	imbi2d	$$⊢y=A\to \left(\left(Ⅎx\phi \to \left(\left[y/x\right]\phi \leftrightarrow \phi \right)\right)\leftrightarrow \left(Ⅎx\phi \to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \phi \right)\right)\right)$$
4		sbft	$$⊢Ⅎx\phi \to \left(\left[y/x\right]\phi \leftrightarrow \phi \right)$$
5	3 4	vtoclg	$$⊢A\in V\to \left(Ⅎx\phi \to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \phi \right)\right)$$
6	5	imp	$$⊢\left(A\in V\wedge Ⅎx\phi \right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \phi \right)$$