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

Theorem csbief 3122
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 3121 . 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 1623    e. wcel 1684   F/_wnfc 2406   _Vcvv 2788   [_csb 3081
This theorem is referenced by:  csbing  3376  csbifg  3593  csbopabg  4094  pofun  4330  csbima12g  5022  csbiotag  5248  csbovg  5889  csbriotag  6317  eqerlem  6692  fsum  12193  fsumcnv  12236  fsumshftm  12243  fsum0diag2  12245  ruclem1  12509  pcmpt  12940  odval  14849  psrass1lem  16123  iundisj2  18906  isibl  19120  dfitg  19124  dvfsumlem2  19374  mpfrcl  19402  fsumdvdsmul  20435  iundisj2fi  23364  iundisj2f  23366  bpolyval  24784  fprodp1fi  25328  fphpd  26899  monotuz  27026  oddcomabszz  27029  fnwe2val  27146  fnwe2lem1  27147  mamufval  27443  csbafv12g  28000  csbaovg  28040
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-3an 936  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