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

Theorem fvmptd 5606
Description: Deduction version of fvmpt 5602. (Contributed by Scott Fenton, 18-Feb-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
Hypotheses
Ref Expression
fvmptd.1  |-  ( ph  ->  F  =  ( x  e.  D  |->  B ) )
fvmptd.2  |-  ( (
ph  /\  x  =  A )  ->  B  =  C )
fvmptd.3  |-  ( ph  ->  A  e.  D )
fvmptd.4  |-  ( ph  ->  C  e.  V )
Assertion
Ref Expression
fvmptd  |-  ( ph  ->  ( F `  A
)  =  C )
Distinct variable groups:    x, A    x, C    x, D    ph, x
Allowed substitution hints:    B( x)    F( x)    V( x)

Proof of Theorem fvmptd
StepHypRef Expression
1 fvmptd.1 . . 3  |-  ( ph  ->  F  =  ( x  e.  D  |->  B ) )
21fveq1d 5527 . 2  |-  ( ph  ->  ( F `  A
)  =  ( ( x  e.  D  |->  B ) `  A ) )
3 fvmptd.3 . . 3  |-  ( ph  ->  A  e.  D )
4 fvmptd.2 . . . . 5  |-  ( (
ph  /\  x  =  A )  ->  B  =  C )
53, 4csbied 3123 . . . 4  |-  ( ph  ->  [_ A  /  x ]_ B  =  C
)
6 fvmptd.4 . . . 4  |-  ( ph  ->  C  e.  V )
75, 6eqeltrd 2357 . . 3  |-  ( ph  ->  [_ A  /  x ]_ B  e.  V
)
8 eqid 2283 . . . 4  |-  ( x  e.  D  |->  B )  =  ( x  e.  D  |->  B )
98fvmpts 5603 . . 3  |-  ( ( A  e.  D  /\  [_ A  /  x ]_ B  e.  V )  ->  ( ( x  e.  D  |->  B ) `  A )  =  [_ A  /  x ]_ B
)
103, 7, 9syl2anc 642 . 2  |-  ( ph  ->  ( ( x  e.  D  |->  B ) `  A )  =  [_ A  /  x ]_ B
)
112, 10, 53eqtrd 2319 1  |-  ( ph  ->  ( F `  A
)  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623    e. wcel 1684   [_csb 3081    e. cmpt 4077   ` cfv 5255
This theorem is referenced by:  fvmptdv2  5613  ttukeylem3  8138  ccatval1  11431  ccatval2  11432  prdsvscafval  13379  mrcval  13512  cidval  13579  subcid  13721  idfu2nd  13751  resf2nd  13769  fuccoval  13837  fucid  13845  homaval  13863  idaval  13890  setcval  13909  setcid  13918  catcval  13928  catcid  13935  prf1  13974  prf2  13976  curf1  13999  curf11  14000  curf2val  14004  hofval  14026  hof2  14031  yonval  14035  yonedalem4a  14049  frmdval  14473  vrmdval  14479  gexval  14889  pj1val  15004  dpjval  15291  sraval  15929  opsrval  16216  lmfval  16962  kgenval  17230  ptval  17265  fcfval  17728  blfval  17947  tmsval  18027  caufval  18701  taylpval  19746  logexprlim  20464  dchrval  20473  dchr1  20496  ballotlemfval  23048  ballotlemsv  23068  esummulc1  23449  esumcvg  23454  ofcval  23460  sigagenval  23501  measinb  23548  indv  23596  indval  23597  indfval  23600  totprobd  23629  probmeasb  23633  cndprobval  23636  dstrvprob  23672  dstfrvinc  23677  dstfrvclim1  23678  cvmliftlem9  23824  relexp0  24025  relexpsucr  24026  rtrclreclem.subset  24042  rtrclreclem.min  24044  dfrtrcl2  24045  areacirc  24931  sgplpte21  26132  sgplpte22  26138  isray2  26153  isray  26154  aishp  26172  fmuldfeqlem1  27712  clim1fr1  27727  climrec  27729  climexp  27731  climneg  27736  itgsinexp  27749  stoweidlem7  27756  stoweidlem17  27766  stoweidlem32  27781  stoweidlem34  27783  wallispilem4  27817  wallispilem5  27818  wallispi  27819  wallispi2lem1  27820  wallispi2lem2  27821  wallispi2  27822  stirlinglem1  27823  stirlinglem2  27824  stirlinglem3  27825  stirlinglem4  27826  stirlinglem5  27827  stirlinglem7  27829  stirlinglem8  27830  stirlinglem10  27832  stirlinglem11  27833  stirlinglem12  27834  stirlinglem13  27835  stirlinglem14  27836  stirlinglem15  27837  cdleme31fv2  30582  tendopl2  30966  tendoi2  30984  erngplus2  30993  erngplus2-rN  31001  hlhilset  32127
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-iota 5219  df-fun 5257  df-fv 5263
  Copyright terms: Public domain W3C validator