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

Theorem csbief 3414
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 3413 . 2  |-  ( A  e.  _V  ->  [_ A  /  x ]_ B  =  C )
61, 5ax-mp 5 1  |-  [_ A  /  x ]_ B  =  C
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    e. wcel 1758   F/_wnfc 2599   _Vcvv 3071   [_csb 3389
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-v 3073  df-sbc 3288  df-csb 3390
This theorem is referenced by:  csbun  3810  csbin  3813  csbingOLD  3814  csbif  3940  csbifgOLD  3941  csbopab  4721  csbopabgALT  4722  pofun  4758  csbima12  5287  csbima12gOLD  5288  csbiota  5511  csbiotagOLD  5512  csbriota  6166  csbov123  6224  csbovgOLD  6226  eqerlem  7236  fsum  13308  fsumcnv  13351  fsumshftm  13359  fsum0diag2  13361  ruclem1  13624  pcmpt  14065  odval  16150  psrass1lem  17562  mpfrcl  17720  mamufval  18401  iundisj2  21156  isibl  21369  dfitg  21373  dvfsumlem2  21625  fsumdvdsmul  22661  disjxpin  26074  iundisj2f  26076  iundisj2fi  26219  fprod  27591  fprodcnv  27631  bpolyval  28329  sbccom2f  29076  fphpd  29296  monotuz  29423  oddcomabszz  29426  fnwe2val  29543  fnwe2lem1  29544  csbafv12g  30184  csbaovg  30227
  Copyright terms: Public domain W3C validator