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

Theorem csbfv 5914
Description: Substitution for a function value. (Contributed by NM, 1-Jan-2006.) (Revised by NM, 20-Aug-2018.)
Assertion
Ref Expression
csbfv  |-  [_ A  /  x ]_ ( F `
 x )  =  ( F `  A
)
Distinct variable group:    x, F
Allowed substitution hint:    A( x)

Proof of Theorem csbfv
StepHypRef Expression
1 csbfv2g 5913 . . 3  |-  ( A  e.  _V  ->  [_ A  /  x ]_ ( F `
 x )  =  ( F `  [_ A  /  x ]_ x ) )
2 csbvarg 3820 . . . 4  |-  ( A  e.  _V  ->  [_ A  /  x ]_ x  =  A )
32fveq2d 5881 . . 3  |-  ( A  e.  _V  ->  ( F `  [_ A  /  x ]_ x )  =  ( F `  A
) )
41, 3eqtrd 2463 . 2  |-  ( A  e.  _V  ->  [_ A  /  x ]_ ( F `
 x )  =  ( F `  A
) )
5 csbprc 3798 . . 3  |-  ( -.  A  e.  _V  ->  [_ A  /  x ]_ ( F `  x )  =  (/) )
6 fvprc 5871 . . 3  |-  ( -.  A  e.  _V  ->  ( F `  A )  =  (/) )
75, 6eqtr4d 2466 . 2  |-  ( -.  A  e.  _V  ->  [_ A  /  x ]_ ( F `  x )  =  ( F `  A ) )
84, 7pm2.61i 167 1  |-  [_ A  /  x ]_ ( F `
 x )  =  ( F `  A
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    = wceq 1437    e. wcel 1868   _Vcvv 3081   [_csb 3395   (/)c0 3761   ` cfv 5597
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-nul 4551  ax-pow 4598
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-br 4421  df-dm 4859  df-iota 5561  df-fv 5605
This theorem is referenced by:  mptcoe1fsupp  18795  mptcoe1matfsupp  19812  mp2pm2mplem4  19819  chfacfscmulfsupp  19869  chfacfpmmulfsupp  19873  cpmidpmatlem3  19882  cayhamlem4  19898  cayleyhamilton1  19902  logbmpt  23711  iuninc  28165  disjxpin  28187  finixpnum  31843  cdlemkid3N  34418  cdlemkid4  34419  cdlemk39s  34424  mccllem  37496
  Copyright terms: Public domain W3C validator