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

Theorem csbconstg 3181
Description: Substitution doesn't affect a constant  B (in which  x is not free). csbconstgf 3180 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 2502 . 2  |-  F/_ x B
21csbconstgf 3180 1  |-  ( A  e.  V  ->  [_ A  /  x ]_ B  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1647    e. wcel 1715   [_csb 3167
This theorem is referenced by:  sbcel1g  3186  sbceq1g  3187  sbcel2g  3188  sbceq2g  3189  csbidmg  3221  sbcbr12g  4175  sbcbr1g  4176  sbcbr2g  4177  csbresg  5061  csbfv12g  5642  csbfv12gALT  5643  csbfv2g  5644  csbov12g  6013  csbov1g  6014  csbov2g  6015  disjpreima  23424  csbcnvg  23436  disjdsct  23493  sbcrel  27487  sbcfun  27493  onfrALTlem5  28054  onfrALTlem4  28055  onfrALTlem5VD  28425  onfrALTlem4VD  28426  csbsngVD  28433  csbxpgVD  28434  csbresgVD  28435  csbrngVD  28436  csbfv12gALTVD  28439  cdlemkid3N  31193  cdlemkid4  31194  cdlemk42  31201
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-v 2875  df-sbc 3078  df-csb 3168
  Copyright terms: Public domain W3C validator