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

Theorem csbiegf 3300
Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 11-Nov-2005.) (Revised by Mario Carneiro, 13-Oct-2016.)
Hypotheses
Ref Expression
csbiegf.1  |-  ( A  e.  V  ->  F/_ x C )
csbiegf.2  |-  ( x  =  A  ->  B  =  C )
Assertion
Ref Expression
csbiegf  |-  ( A  e.  V  ->  [_ A  /  x ]_ B  =  C )
Distinct variable groups:    x, A    x, V
Allowed substitution hints:    B( x)    C( x)

Proof of Theorem csbiegf
StepHypRef Expression
1 csbiegf.2 . . 3  |-  ( x  =  A  ->  B  =  C )
21ax-gen 1594 . 2  |-  A. x
( x  =  A  ->  B  =  C )
3 csbiegf.1 . . 3  |-  ( A  e.  V  ->  F/_ x C )
4 csbiebt 3296 . . 3  |-  ( ( A  e.  V  /\  F/_ x C )  -> 
( A. x ( x  =  A  ->  B  =  C )  <->  [_ A  /  x ]_ B  =  C )
)
53, 4mpdan 661 . 2  |-  ( A  e.  V  ->  ( A. x ( x  =  A  ->  B  =  C )  <->  [_ A  /  x ]_ B  =  C ) )
62, 5mpbii 211 1  |-  ( A  e.  V  ->  [_ A  /  x ]_ B  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1360    = wceq 1362    e. wcel 1755   F/_wnfc 2556   [_csb 3276
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-sbc 3176  df-csb 3277
This theorem is referenced by:  csbief  3301  sbcco3g  3683  csbco3g  3684  csbungOLD  3698  csbopg  4065  fmptcof  5864  fmpt2co  6645  sumsn  13200  pcmpt  13936  elmptrab  19241  dvfsumrlim3  21346  itgsubstlem  21361  itgsubst  21362  ifeqeqx  25725  disjunsn  25759  prodsn  27319  sbcaltop  27858  bpolylem  28037  unirep  28447  monotuz  29124  oddcomabszz  29127  cdleme31so  33593  cdleme31sn  33594  cdleme31sn1  33595  cdleme31se  33596  cdleme31se2  33597  cdleme31sc  33598  cdleme31sde  33599  cdleme31sn2  33603  cdlemeg47rv2  33724  cdlemk41  34134
  Copyright terms: Public domain W3C validator