Theorem csbtt

Description: Substitution doesn't affect a constant B (in which x is not free). (Contributed by Mario Carneiro, 14-Oct-2016)

	Ref	Expression
Assertion	csbtt	$$⊢\left(A\in V\wedge \underset{\_}{Ⅎ}xB\right)\to ⦋A/x⦌B=B$$

Proof

Step	Hyp	Ref	Expression
1		df-csb	$$⊢⦋A/x⦌B=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right\}$$
2		nfcr	$$⊢\underset{\_}{Ⅎ}xB\to Ⅎxy\in B$$
3		sbctt	$$⊢\left(A\in V\wedge Ⅎxy\in B\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\leftrightarrow y\in B\right)$$
4	2 3	sylan2	$$⊢\left(A\in V\wedge \underset{\_}{Ⅎ}xB\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\leftrightarrow y\in B\right)$$
5	4	abbi1dv	$$⊢\left(A\in V\wedge \underset{\_}{Ⅎ}xB\right)\to \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right\}=B$$
6	1 5	syl5eq	$$⊢\left(A\in V\wedge \underset{\_}{Ⅎ}xB\right)\to ⦋A/x⦌B=B$$