Theorem csbconstg 3411

Description: Substitution doesn't affect a constant B (in which x does not occur). csbconstgf 3410 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 2616	. 2 |- F/_ x B
2	1	csbconstgf 3410	1 |- ( A e. V -> [_ A / x ]_ B = B )

Syntax hints:   -> wi 4   = wceq 1370   e. wcel 1758   [_csb 3398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080  df-sbc 3295  df-csb 3399

This theorem is referenced by:  csb0  3785  sbcel1g  3792  sbceq1g  3793  sbcel2  3794  sbcel2gOLD  3795  sbceq2g  3796  csbidm  3809  csbidmgOLD  3810  sbcbr  4456  sbcbr12g  4457  sbcbr1g  4458  sbcbr2g  4459  csbmpt12  4733  csbmpt2  4734  sbcrel  5037  csbcnvgALT  5135  csbres  5224  csbresgOLD  5225  csbrn  5410  sbcfung  5552  csbfv12  5837  csbfv12gOLD  5838  csbfv2g  5839  csbov  6235  csbov12g  6237  csbov1g  6238  csbov2g  6239  csbwrdg  12379  gsummptif1n0  16589  evl1gsumdlem  17925  disjpreima  26106  csbconstgi  29096  elfvmptrab  30326  rusgrasn  30728  coe1fzgsumdlem  31013  onfrALTlem5  31605  onfrALTlem4  31606  csbfv12gALTOLD  31912  onfrALTlem5VD  31976  onfrALTlem4VD  31977  csbsngVD  31984  csbxpgVD  31985  csbresgVD  31986  csbrngVD  31987  csbfv12gALTVD  31990  cdlemkid3N  34940  cdlemkid4  34941  cdlemk42  34948