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

Theorem csbied2 3458
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 22 . . . 4  |-  ( x  =  A  ->  x  =  A )
3 csbied2.2 . . . 4  |-  ( ph  ->  A  =  B )
42, 3sylan9eqr 2525 . . 3  |-  ( (
ph  /\  x  =  A )  ->  x  =  B )
5 csbied2.3 . . 3  |-  ( (
ph  /\  x  =  B )  ->  C  =  D )
64, 5syldan 470 . 2  |-  ( (
ph  /\  x  =  A )  ->  C  =  D )
71, 6csbied 3457 1  |-  ( ph  ->  [_ A  /  x ]_ C  =  D
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1374    e. wcel 1762   [_csb 3430
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-v 3110  df-sbc 3327  df-csb 3431
This theorem is referenced by:  prdsval  14701  cidfval  14922  monfval  14979  idfuval  15094  isnat  15165  fucco  15180  catcval  15272  xpcval  15295  1stfval  15309  2ndfval  15312  prfval  15317  evlf2  15336  curfval  15341  hofval  15370  ipoval  15632
  Copyright terms: Public domain W3C validator