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

Theorem csbief 3460
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 3459 . 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 1379    e. wcel 1767   F/_wnfc 2615   _Vcvv 3113   [_csb 3435
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-sbc 3332  df-csb 3436
This theorem is referenced by:  csbie  3461  csbun  3857  csbin  3860  csbingOLD  3861  csbif  3989  csbifgOLD  3990  csbopab  4779  csbopabgALT  4780  pofun  4816  csbima12  5352  csbima12gOLD  5353  csbiota  5578  csbiotagOLD  5579  csbriota  6255  csbov123  6313  csbovgOLD  6315  eqerlem  7340  fsum  13501  fsumcnv  13547  fsumshftm  13555  fsum0diag2  13557  ruclem1  13821  pcmpt  14266  odval  16354  psrass1lem  17800  mpfrcl  17958  mamufval  18654  iundisj2  21694  isibl  21907  dfitg  21911  dvfsumlem2  22163  fsumdvdsmul  23199  disjxpin  27120  iundisj2f  27122  iundisj2fi  27270  fprod  28650  fprodcnv  28690  bpolyval  29388  sbccom2f  30135  fphpd  30354  monotuz  30481  oddcomabszz  30484  fnwe2val  30599  fnwe2lem1  30600  csbafv12g  31689  csbaovg  31732
  Copyright terms: Public domain W3C validator