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

Theorem csbief 3308
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 3307 . 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 1369    e. wcel 1756   F/_wnfc 2561   _Vcvv 2967   [_csb 3283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-sbc 3182  df-csb 3284
This theorem is referenced by:  csbun  3704  csbin  3707  csbingOLD  3708  csbif  3834  csbifgOLD  3835  csbopab  4615  csbopabgALT  4616  pofun  4652  csbima12  5181  csbima12gOLD  5182  csbiota  5405  csbiotagOLD  5406  csbriota  6059  csbov123  6117  csbovgOLD  6119  eqerlem  7125  fsum  13189  fsumcnv  13232  fsumshftm  13240  fsum0diag2  13242  ruclem1  13505  pcmpt  13946  odval  16028  psrass1lem  17424  mpfrcl  17579  mamufval  18258  iundisj2  21005  isibl  21218  dfitg  21222  dvfsumlem2  21474  fsumdvdsmul  22510  disjxpin  25881  iundisj2f  25883  iundisj2fi  26032  fprod  27405  fprodcnv  27445  bpolyval  28143  sbccom2f  28888  fphpd  29108  monotuz  29235  oddcomabszz  29238  fnwe2val  29355  fnwe2lem1  29356  csbafv12g  29996  csbaovg  30039
  Copyright terms: Public domain W3C validator