Theorem csbconstg 3225

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

Syntax hints:   -> wi 4   = wceq 1649   e. wcel 1721   [_csb 3211

This theorem is referenced by:  sbcel1g  3230  sbceq1g  3231  sbcel2g  3232  sbceq2g  3233  csbidmg  3264  sbcbr12g  4222  sbcbr1g  4223  sbcbr2g  4224  csbresg  5108  csbfv12g  5697  csbfv12gALT  5698  csbfv2g  5699  csbov12g  6072  csbov1g  6073  csbov2g  6074  disjpreima  23979  csbcnvg  23990  disjdsct  24043  sbcrel  27848  sbcfun  27854  onfrALTlem5  28339  onfrALTlem4  28340  onfrALTlem5VD  28706  onfrALTlem4VD  28707  csbsngVD  28714  csbxpgVD  28715  csbresgVD  28716  csbrngVD  28717  csbfv12gALTVD  28720  cdlemkid3N  31415  cdlemkid4  31416  cdlemk42  31423

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-sbc 3122  df-csb 3212