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	$⊢ (A \in V \land \underline{Ⅎ} x B) \to ⦋ A / x ⦌ B = B$

Step	Hyp	Ref	Expression
1		df-csb	$⊢ ⦋ A / x ⦌ B = \{y \| \underset{˙}{[} A / x \underset{˙}{]} y \in B\}$
2		nfcr	$⊢ \underline{Ⅎ} x B \to Ⅎ x y \in B$
3		sbctt	$⊢ (A \in V \land Ⅎ x y \in B) \to (\underset{˙}{[} A / x \underset{˙}{]} y \in B \leftrightarrow y \in B)$
4	2 3	sylan2	$⊢ (A \in V \land \underline{Ⅎ} x B) \to (\underset{˙}{[} A / x \underset{˙}{]} y \in B \leftrightarrow y \in B)$
5	4	eqabcdv	$⊢ (A \in V \land \underline{Ⅎ} x B) \to \{y \| \underset{˙}{[} A / x \underset{˙}{]} y \in B\} = B$
6	1 5	eqtrid	$⊢ (A \in V \land \underline{Ⅎ} x B) \to ⦋ A / x ⦌ B = B$

Metamath Proof Explorer