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

Theorem csbiegf 3399
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 1641 . 2  |-  A. x
( x  =  A  ->  B  =  C )
3 csbiegf.1 . . 3  |-  ( A  e.  V  ->  F/_ x C )
4 csbiebt 3395 . . 3  |-  ( ( A  e.  V  /\  F/_ x C )  -> 
( A. x ( x  =  A  ->  B  =  C )  <->  [_ A  /  x ]_ B  =  C )
)
53, 4mpdan 668 . 2  |-  ( A  e.  V  ->  ( A. x ( x  =  A  ->  B  =  C )  <->  [_ A  /  x ]_ B  =  C ) )
62, 5mpbii 213 1  |-  ( A  e.  V  ->  [_ A  /  x ]_ B  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 186   A.wal 1405    = wceq 1407    e. wcel 1844   F/_wnfc 2552   [_csb 3375
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382
This theorem depends on definitions:  df-bi 187  df-an 371  df-3an 978  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-v 3063  df-sbc 3280  df-csb 3376
This theorem is referenced by:  csbief  3400  sbcco3g  3795  csbco3g  3796  csbopg  4179  fmptcof  6046  fmpt2co  6869  sumsn  13714  prodsn  13921  bpolylem  13995  pcmpt  14622  chfacfpmmulfsupp  19658  elmptrab  20622  dvfsumrlim3  22728  itgsubstlem  22743  itgsubst  22744  nbgraopALT  24853  ifeqeqx  27853  disjunsn  27899  sbcaltop  30332  unirep  31498  cdleme31so  33411  cdleme31sn  33412  cdleme31sn1  33413  cdleme31se  33414  cdleme31se2  33415  cdleme31sc  33416  cdleme31sde  33417  cdleme31sn2  33421  cdlemeg47rv2  33542  cdlemk41  33952  monotuz  35251  oddcomabszz  35254  sumsnf  36951  prodsnf  36968
  Copyright terms: Public domain W3C validator