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

Theorem csbief 3292
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 11 . . 3  |-  ( A  e.  _V  ->  F/_ x C )
4 csbief.3 . . 3  |-  ( x  =  A  ->  B  =  C )
53, 4csbiegf 3291 . 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 1652    e. wcel 1725   F/_wnfc 2559   _Vcvv 2956   [_csb 3251
This theorem is referenced by:  csbing  3548  csbifg  3767  csbopabg  4283  pofun  4519  csbima12g  5213  csbiotag  5447  csbovg  6112  csbriotag  6562  eqerlem  6937  fsum  12514  fsumcnv  12557  fsumshftm  12564  fsum0diag2  12566  ruclem1  12830  pcmpt  13261  odval  15172  psrass1lem  16442  iundisj2  19443  isibl  19657  dfitg  19661  dvfsumlem2  19911  mpfrcl  19939  fsumdvdsmul  20980  disjxpin  24028  iundisj2f  24030  iundisj2fi  24153  fprod  25267  fprodcnv  25307  bpolyval  26095  fphpd  26877  monotuz  27004  oddcomabszz  27007  fnwe2val  27124  fnwe2lem1  27125  mamufval  27420  csbafv12g  27977  csbaovg  28020
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2958  df-sbc 3162  df-csb 3252
  Copyright terms: Public domain W3C validator