MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  csbconstg Structured version   Unicode version

Theorem csbconstg 3453
Description: Substitution doesn't affect a constant  B (in which  x does not occur). csbconstgf 3452 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
StepHypRef Expression
1 nfcv 2629 . 2  |-  F/_ x B
21csbconstgf 3452 1  |-  ( A  e.  V  ->  [_ A  /  x ]_ B  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    e. wcel 1767   [_csb 3440
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3120  df-sbc 3337  df-csb 3441
This theorem is referenced by:  csb0  3827  sbcel1g  3834  sbceq1g  3835  sbcel2  3836  sbcel2gOLD  3837  sbceq2g  3838  csbidm  3851  csbidmgOLD  3852  sbcbr  4506  sbcbr12g  4507  sbcbr1g  4508  sbcbr2g  4509  csbmpt12  4787  csbmpt2  4788  sbcrel  5095  csbcnvgALT  5193  csbres  5282  csbresgOLD  5283  csbrn  5474  sbcfung  5617  csbfv12  5907  csbfv12gOLD  5908  csbfv2g  5909  elfvmptrab  5978  csbov  6327  csbov12g  6329  csbov1g  6330  csbov2g  6331  csbwrdg  12551  gsummptif1n0  16866  coe1fzgsumdlem  18213  evl1gsumdlem  18262  rusgrasn  24768  disjpreima  27268  csbconstgi  30449  onfrALTlem5  32795  onfrALTlem4  32796  csbfv12gALTOLD  33102  onfrALTlem5VD  33166  onfrALTlem4VD  33167  csbsngVD  33174  csbxpgVD  33175  csbresgVD  33176  csbrngVD  33177  csbfv12gALTVD  33180  cdlemkid3N  36130  cdlemkid4  36131  cdlemk42  36138
  Copyright terms: Public domain W3C validator