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

Theorem csbiegf 3414
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 1592 . 2  |-  A. x
( x  =  A  ->  B  =  C )
3 csbiegf.1 . . 3  |-  ( A  e.  V  ->  F/_ x C )
4 csbiebt 3410 . . 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 211 1  |-  ( A  e.  V  ->  [_ A  /  x ]_ B  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1368    = wceq 1370    e. wcel 1758   F/_wnfc 2600   [_csb 3390
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1954  ax-ext 2431
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2602  df-v 3074  df-sbc 3289  df-csb 3391
This theorem is referenced by:  csbief  3415  sbcco3g  3798  csbco3g  3799  csbungOLD  3813  csbopg  4180  fmptcof  5981  fmpt2co  6761  sumsn  13330  pcmpt  14067  elmptrab  19527  dvfsumrlim3  21633  itgsubstlem  21648  itgsubst  21649  ifeqeqx  26049  disjunsn  26082  prodsn  27612  sbcaltop  28151  bpolylem  28330  unirep  28749  monotuz  29425  oddcomabszz  29428  chfacfpmmulfsupp  31330  cdleme31so  34342  cdleme31sn  34343  cdleme31sn1  34344  cdleme31se  34345  cdleme31se2  34346  cdleme31sc  34347  cdleme31sde  34348  cdleme31sn2  34352  cdlemeg47rv2  34473  cdlemk41  34883
  Copyright terms: Public domain W3C validator