This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem csbconstgf

Description: Substitution doesn't affect a constant B (in which x is not free). (Contributed by NM, 10-Nov-2005)

		Ref	Expression
	Hypothesis	csbconstgf.1	$⊢ \underline{Ⅎ} x B$
	Assertion	csbconstgf	$⊢ A \in V \to ⦋ A / x ⦌ B = B$

Step	Hyp	Ref	Expression
1		csbconstgf.1	$⊢ \underline{Ⅎ} x B$
2		csbtt	$⊢ (A \in V \land \underline{Ⅎ} x B) \to ⦋ A / x ⦌ B = B$
3	1 2	mpan2	$⊢ A \in V \to ⦋ A / x ⦌ B = B$