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 _xB
Assertion csbconstgf AVA/xB=B

Proof

Step Hyp Ref Expression
1 csbconstgf.1 _xB
2 csbtt AV_xBA/xB=B
3 1 2 mpan2 AVA/xB=B