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

Theorem csbied2 3296
Description: Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by Mario Carneiro, 2-Jan-2017.)
Hypotheses
Ref Expression
csbied2.1  |-  ( ph  ->  A  e.  V )
csbied2.2  |-  ( ph  ->  A  =  B )
csbied2.3  |-  ( (
ph  /\  x  =  B )  ->  C  =  D )
Assertion
Ref Expression
csbied2  |-  ( ph  ->  [_ A  /  x ]_ C  =  D
)
Distinct variable groups:    x, A    ph, x    x, D
Allowed substitution hints:    B( x)    C( x)    V( x)

Proof of Theorem csbied2
StepHypRef Expression
1 csbied2.1 . 2  |-  ( ph  ->  A  e.  V )
2 id 21 . . . 4  |-  ( x  =  A  ->  x  =  A )
3 csbied2.2 . . . 4  |-  ( ph  ->  A  =  B )
42, 3sylan9eqr 2492 . . 3  |-  ( (
ph  /\  x  =  A )  ->  x  =  B )
5 csbied2.3 . . 3  |-  ( (
ph  /\  x  =  B )  ->  C  =  D )
64, 5syldan 458 . 2  |-  ( (
ph  /\  x  =  A )  ->  C  =  D )
71, 6csbied 3295 1  |-  ( ph  ->  [_ A  /  x ]_ C  =  D
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    = wceq 1653    e. wcel 1726   [_csb 3253
This theorem is referenced by:  prdsval  13680  cidfval  13903  monfval  13960  idfuval  14075  isnat  14146  fucco  14161  catcval  14253  xpcval  14276  1stfval  14290  2ndfval  14293  prfval  14298  evlf2  14317  curfval  14322  hofval  14351  ipoval  14582
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-sbc 3164  df-csb 3254
  Copyright terms: Public domain W3C validator