Theorem csbconstg 3388

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

Syntax hints:   -> wi 4   = wceq 1407   e. wcel 1844   [_csb 3375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382

This theorem depends on definitions:  df-bi 187  df-an 371  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-v 3063  df-sbc 3280  df-csb 3376

This theorem is referenced by:  csb0  3778  sbcel1g  3783  sbceq1g  3784  sbcel2  3785  sbceq2g  3786  csbidm  3798  sbcbr  4449  sbcbr12g  4450  sbcbr1g  4451  sbcbr2g  4452  csbmpt12  4726  csbmpt2  4727  sbcrel  4912  csbcnvgALT  5010  csbres  5099  csbrn  5287  sbcfung  5594  csbfv12  5886  csbfv2g  5887  elfvmptrab  5957  csbov  6315  csbov12g  6316  csbov1g  6317  csbov2g  6318  csbwrdg  12625  gsummptif1n0  17316  coe1fzgsumdlem  18665  evl1gsumdlem  18714  rusgrasn  25374  disjpreima  27889  esum2dlem  28552  f1omptsnlem  31265  relowlpssretop  31294  csbconstgi  31817  cdlemkid3N  33965  cdlemkid4  33966  cdlemk42  33973  brtrclfv2  35719  cotrclrcl  35734  frege77  35934  sbcel2gOLD  36349  onfrALTlem5  36351  onfrALTlem4  36352  csbfv12gALTOLD  36660  csbresgOLD  36663  onfrALTlem5VD  36729  onfrALTlem4VD  36730  csbsngVD  36737  csbxpgVD  36738  csbresgVD  36739  csbrngVD  36740  csbfv12gALTVD  36743  iccelpart  37713