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

Theorem csbconstg 3095
Description: Substitution doesn't affect a constant  B (in which  x is not free). csbconstgf 3094 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 2419 . 2  |-  F/_ x B
21csbconstgf 3094 1  |-  ( A  e.  V  ->  [_ A  /  x ]_ B  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684   [_csb 3081
This theorem is referenced by:  sbcel1g  3100  sbceq1g  3101  sbcel2g  3102  sbceq2g  3103  csbidmg  3135  sbcbr12g  4073  sbcbr1g  4074  sbcbr2g  4075  csbresg  4958  csbfv12g  5535  csbfv12gALT  5536  csbfv2g  5537  csbov12g  5890  csbov1g  5891  csbov2g  5892  csbcnvg  23198  disjpreima  23361  disjdsct  23369  sbcrel  27979  sbcfun  27985  onfrALTlem5  28307  onfrALTlem4  28308  onfrALTlem5VD  28661  onfrALTlem4VD  28662  csbsngVD  28669  csbxpgVD  28670  csbresgVD  28671  csbrngVD  28672  csbfv12gALTVD  28675  cdlemkid3N  31122  cdlemkid4  31123  cdlemk42  31130
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-sbc 2992  df-csb 3082
  Copyright terms: Public domain W3C validator