Metamath Proof Explorer


Theorem csbconstg

Description: Substitution doesn't affect a constant B (in which x does not occur). csbconstgf with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012)

Ref Expression
Assertion csbconstg A V A / x B = B

Proof

Step Hyp Ref Expression
1 nfcv _ x B
2 1 csbconstgf A V A / x B = B