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 2603	. 2 |- F/_ x B
2	1	csbconstgf 3387	1 |- ( A e. V -> [_ A / x ]_ B = B )

Syntax hints:   -> wi 4   = wceq 1455   e. wcel 1898   [_csb 3375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-sbc 3280  df-csb 3376

This theorem is referenced by:  csb0  3783  sbcel1g  3788  sbceq1g  3789  sbcel2  3790  sbceq2g  3791  csbidm  3803  sbcbr  4471  sbcbr12g  4472  sbcbr1g  4473  sbcbr2g  4474  csbmpt12  4752  csbmpt2  4753  sbcrel  4943  csbcnvgALT  5041  csbres  5130  csbrn  5320  sbcfung  5628  csbfv12  5927  csbfv2g  5928  elfvmptrab  5999  csbov  6355  csbov12g  6356  csbov1g  6357  csbov2g  6358  csbwrdg  12738  gsummptif1n0  17653  coe1fzgsumdlem  18950  evl1gsumdlem  18999  rusgrasn  25729  disjpreima  28248  esum2dlem  28964  csbopg2  31771  csbwrecsg  31774  csbrecsg  31775  csbrdgg  31776  csbmpt22g  31778  f1omptsnlem  31784  relowlpssretop  31813  rdgeqoa  31819  csbfinxpg  31826  csbconstgi  32403  cdlemkid3N  34546  cdlemkid4  34547  cdlemk42  34554  brtrclfv2  36365  cotrclrcl  36380  frege77  36582  sbcel2gOLD  36951  onfrALTlem5  36953  onfrALTlem4  36954  csbfv12gALTOLD  37254  csbresgOLD  37257  onfrALTlem5VD  37323  onfrALTlem4VD  37324  csbsngVD  37331  csbxpgVD  37332  csbresgVD  37333  csbrngVD  37334  csbfv12gALTVD  37337  disjinfi  37522  iccelpart  38882