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

Theorem csbief 3135
Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 26-Nov-2005.) (Revised by Mario Carneiro, 13-Oct-2016.)
Hypotheses
Ref Expression
csbief.1  |-  A  e. 
_V
csbief.2  |-  F/_ x C
csbief.3  |-  ( x  =  A  ->  B  =  C )
Assertion
Ref Expression
csbief  |-  [_ A  /  x ]_ B  =  C
Distinct variable group:    x, A
Allowed substitution hints:    B( x)    C( x)

Proof of Theorem csbief
StepHypRef Expression
1 csbief.1 . 2  |-  A  e. 
_V
2 csbief.2 . . . 4  |-  F/_ x C
32a1i 10 . . 3  |-  ( A  e.  _V  ->  F/_ x C )
4 csbief.3 . . 3  |-  ( x  =  A  ->  B  =  C )
53, 4csbiegf 3134 . 2  |-  ( A  e.  _V  ->  [_ A  /  x ]_ B  =  C )
61, 5ax-mp 8 1  |-  [_ A  /  x ]_ B  =  C
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    e. wcel 1696   F/_wnfc 2419   _Vcvv 2801   [_csb 3094
This theorem is referenced by:  csbing  3389  csbifg  3606  csbopabg  4110  pofun  4346  csbima12g  5038  csbiotag  5264  csbovg  5905  csbriotag  6333  eqerlem  6708  fsum  12209  fsumcnv  12252  fsumshftm  12259  fsum0diag2  12261  ruclem1  12525  pcmpt  12956  odval  14865  psrass1lem  16139  iundisj2  18922  isibl  19136  dfitg  19140  dvfsumlem2  19390  mpfrcl  19418  fsumdvdsmul  20451  iundisj2fi  23379  iundisj2f  23381  fprod  24164  bpolyval  24856  fprodp1fi  25431  fphpd  27002  monotuz  27129  oddcomabszz  27132  fnwe2val  27249  fnwe2lem1  27250  mamufval  27546  csbafv12g  28105  csbaovg  28148
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-sbc 3005  df-csb 3095
  Copyright terms: Public domain W3C validator