Theorem csbconstg 2959

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

Assertion

Ref	Expression
csbconstg	|- ( A e. V -> [_ A / x ]_ B = B )

Distinct variable group:   x, B

Allowed substitution hints:   A( x)   V( x)

Proof of Theorem csbconstg

Step	Hyp	Ref	Expression
1		nfcv 2235	. 2 |- F/_ x B
2	1	csbconstgf 2958	1 |- ( A e. V -> [_ A / x ]_ B = B )

Syntax hints:   -> wi 4   = wceq 1296   e. wcel 1445   [_csb 2947

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-v 2635  df-sbc 2855  df-csb 2948

This theorem is referenced by:  sbcel1g  2964  sbceq1g  2965  sbcel2g  2966  sbceq2g  2967  csbidmg  2998  sbcbr12g  3917  sbcbr1g  3918  sbcbr2g  3919  sbcrel  4553  csbcnvg  4651  csbresg  4748  sbcfung  5073  csbfv12g  5375  csbfv2g  5376  elfvmptrab  5434  csbov12g  5726  csbov1g  5727  csbov2g  5728