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

Theorem csbiegf 3227
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 1552 . 2  |-  A. x
( x  =  A  ->  B  =  C )
3 csbiegf.1 . . 3  |-  ( A  e.  V  ->  F/_ x C )
4 csbiebt 3223 . . 3  |-  ( ( A  e.  V  /\  F/_ x C )  -> 
( A. x ( x  =  A  ->  B  =  C )  <->  [_ A  /  x ]_ B  =  C )
)
53, 4mpdan 650 . 2  |-  ( A  e.  V  ->  ( A. x ( x  =  A  ->  B  =  C )  <->  [_ A  /  x ]_ B  =  C ) )
62, 5mpbii 203 1  |-  ( A  e.  V  ->  [_ A  /  x ]_ B  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wal 1546    = wceq 1649    e. wcel 1717   F/_wnfc 2503   [_csb 3187
This theorem is referenced by:  csbief  3228  sbcco3g  3241  csbco3g  3243  fmptcof  5834  fmpt2co  6362  sumsn  12454  pcmpt  13181  elmptrab  17773  dvfsumrlim3  19777  itgsubstlem  19792  itgsubst  19793  ifeqeqx  23838  sbcung  24896  sbcopg  24898  prodsn  25058  sbcaltop  25533  bpolylem  25801  unirep  26098  monotuz  26688  oddcomabszz  26691  cdleme31so  30544  cdleme31sn  30545  cdleme31sn1  30546  cdleme31se  30547  cdleme31se2  30548  cdleme31sc  30549  cdleme31sde  30550  cdleme31sn2  30554  cdlemeg47rv2  30675  cdlemk41  31085
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-v 2894  df-sbc 3098  df-csb 3188
  Copyright terms: Public domain W3C validator