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

Theorem fvmptd 5940
Description: Deduction version of fvmpt 5934. (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 5853 . 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 3402 . . . 4  |-  ( ph  ->  [_ A  /  x ]_ B  =  C
)
6 fvmptd.4 . . . 4  |-  ( ph  ->  C  e.  V )
75, 6eqeltrd 2492 . . 3  |-  ( ph  ->  [_ A  /  x ]_ B  e.  V
)
8 eqid 2404 . . . 4  |-  ( x  e.  D  |->  B )  =  ( x  e.  D  |->  B )
98fvmpts 5937 . . 3  |-  ( ( A  e.  D  /\  [_ A  /  x ]_ B  e.  V )  ->  ( ( x  e.  D  |->  B ) `  A )  =  [_ A  /  x ]_ B
)
103, 7, 9syl2anc 661 . 2  |-  ( ph  ->  ( ( x  e.  D  |->  B ) `  A )  =  [_ A  /  x ]_ B
)
112, 10, 53eqtrd 2449 1  |-  ( ph  ->  ( F `  A
)  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1407    e. wcel 1844   [_csb 3375    |-> cmpt 4455   ` cfv 5571
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-9 1848  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382  ax-sep 4519  ax-nul 4527  ax-pr 4632
This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-3an 978  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-eu 2244  df-mo 2245  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-ne 2602  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3063  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3741  df-if 3888  df-sn 3975  df-pr 3977  df-op 3981  df-uni 4194  df-br 4398  df-opab 4456  df-mpt 4457  df-id 4740  df-xp 4831  df-rel 4832  df-cnv 4833  df-co 4834  df-dm 4835  df-iota 5535  df-fun 5573  df-fv 5579
This theorem is referenced by:  fvmptdv2  5949  mpt2curryvald  7004  ttukeylem3  8925  ccatval1  12651  ccatval2  12652  repswsymb  12804  relexp1g  13010  rtrclreclem2  13043  rtrclreclem4  13045  dfrtrcl2  13046  prdsvscafval  15096  mrcval  15226  cidval  15293  isofval  15372  isofn  15390  cicfval  15412  subcid  15462  idfu2nd  15492  resf2nd  15510  fuccoval  15578  fucid  15586  initoval  15602  termoval  15603  zerooval  15604  homaval  15636  idaval  15663  setcval  15682  setcid  15691  catcval  15701  catcid  15708  estrcval  15719  estrcid  15729  funcestrcsetclem1  15735  funcsetcestrclem1  15749  prf1  15795  prf2  15797  curf1  15820  curf11  15821  curf2val  15825  hofval  15847  hof2  15852  yonval  15856  yonedalem4a  15870  frmdval  16345  vrmdval  16351  pmtrdifwrdellem3  16834  gexval  16924  pj1val  17039  dpjval  17427  sraval  18144  opsrval  18461  cply1mul  18657  cply1coe0  18663  cply1coe0bi  18664  gsummoncoe1  18668  evls1sca  18682  frlmphl  19110  mat1rhmval  19275  scmatrhmval  19323  mvmulfv  19340  mavmulfv  19342  mdetuni0  19417  mat2pmatval  19519  m2cpm  19536  cpm2mval  19545  m2cpminvid2lem  19549  decpmatid  19565  decpmatmullem  19566  pmatcollpw2lem  19572  monmatcollpw  19574  pmatcollpw3fi1lem1  19581  pm2mpfval  19591  mply1topmatval  19599  mp2pm2mplem1  19601  mp2pm2mplem4  19604  pm2mpmhmlem2  19614  chpmatval  19626  chfacfscmul0  19653  chfacfscmulgsum  19655  chfacfpmmul0  19657  chfacfpmmulgsum  19659  lmfval  20028  kgenval  20330  ptval  20365  fcfval  20828  cnextfval  20856  ustval  20999  utopval  21029  ustuqtoplem  21036  utopsnneiplem  21044  tusval  21063  blfvalps  21180  tmsval  21278  metuvalOLD  21346  metuval  21347  caufval  22008  rrxmvallem  22125  rrxmval  22126  taylpval  23056  efgh  23222  lgamgulmlem2  23687  lgamcvglem  23697  logexprlim  23883  dchrval  23892  dchr1  23915  mirval  24425  mirfv  24426  israg  24464  perpln1  24477  perpln2  24478  isperp  24479  ishpg  24520  midf  24537  ismidb  24539  lmif  24546  islmib  24548  edgval  24768  wlkiswwlk2lem2  25121  clwlkisclwwlklem2fv1  25211  clwlkisclwwlklem2fv2  25212  sgnsval  28183  metidval  28335  pstmval  28340  qqhvval  28429  indv  28473  indval  28474  indfval  28477  esummulc1  28541  esumcvg  28546  ofcval  28559  sigagenval  28601  measinb  28682  omsval  28754  omsfval  28755  omssubadd  28761  carsgval  28764  sitgfval  28802  eulerpartlemsv1  28814  eulerpartlems  28818  eulerpartlemgvv  28834  fibp1  28859  totprobd  28884  probmeasb  28888  cndprobval  28891  dstrvprob  28929  dstfrvinc  28934  dstfrvclim1  28935  ballotlemfval  28947  ballotlemsv  28967  gsumnunsn  29012  signsply0  29027  signstfval  29040  afsval  29075  cvmliftlem9  29603  mvrsval  29730  mrsubfval  29733  mrsubval  29734  msubfval  29749  msubval  29750  msrval  29763  fwddifval  30513  fwddifnval  30514  bj-finsumval0  31240  mblfinlem2  31437  areacirc  31496  cdleme31fv2  33425  tendopl2  33809  tendoi2  33827  erngplus2  33836  erngplus2-rN  33844  hlhilset  34970  itgpowd  35559  iunrelexpmin1  35700  iunrelexpmin2  35704  dvgrat  36054  radcnvrat  36056  hashnzfzclim  36088  binomcxplemnn0  36115  binomcxplemrat  36116  binomcxplemfrat  36117  binomcxplemradcnv  36118  binomcxplemcvg  36120  binomcxplemdvsum  36121  binomcxplemnotnn0  36122  fmuldfeqlem1  36957  clim1fr1  36988  climrec  36990  climexp  36992  climneg  36997  mullimcf  37010  divcnvg  37014  sumnnodd  37017  expfac  37044  cncfshift  37057  icccncfext  37071  cncfioobdlem  37080  dvsinax  37089  fperdvper  37096  dvcosax  37104  ioodvbdlimc1lem1  37109  ioodvbdlimc1lem2  37110  ioodvbdlimc2lem  37112  dvnmul  37121  dvnprodlem1  37124  dvnprodlem2  37125  dvnprodlem3  37126  itgsinexp  37134  itgcoscmulx  37149  itgsincmulx  37154  itgsubsticclem  37155  itgsubsticc  37156  itgiccshift  37160  stoweidlem7  37170  stoweidlem17  37180  stoweidlem32  37195  stoweidlem34  37197  wallispilem4  37231  wallispilem5  37232  wallispi  37233  wallispi2lem1  37234  wallispi2lem2  37235  wallispi2  37236  stirlinglem1  37237  stirlinglem2  37238  stirlinglem3  37239  stirlinglem4  37240  stirlinglem5  37241  stirlinglem7  37243  stirlinglem8  37244  stirlinglem10  37246  stirlinglem11  37247  stirlinglem12  37248  stirlinglem13  37249  stirlinglem14  37250  stirlinglem15  37251  dirkerval2  37257  dirkercncflem2  37267  fourierdlem7  37277  fourierdlem13  37283  fourierdlem14  37284  fourierdlem16  37286  fourierdlem18  37288  fourierdlem19  37289  fourierdlem21  37291  fourierdlem22  37292  fourierdlem26  37296  fourierdlem37  37307  fourierdlem39  37309  fourierdlem41  37311  fourierdlem48  37318  fourierdlem49  37319  fourierdlem50  37320  fourierdlem51  37321  fourierdlem53  37323  fourierdlem62  37332  fourierdlem63  37333  fourierdlem65  37335  fourierdlem73  37343  fourierdlem74  37344  fourierdlem75  37345  fourierdlem76  37346  fourierdlem79  37349  fourierdlem81  37351  fourierdlem82  37352  fourierdlem83  37353  fourierdlem84  37354  fourierdlem88  37358  fourierdlem89  37359  fourierdlem90  37360  fourierdlem91  37361  fourierdlem92  37362  fourierdlem93  37363  fourierdlem97  37367  fourierdlem101  37371  fourierdlem103  37373  fourierdlem104  37374  fourierdlem111  37381  fourierdlem112  37382  fouriersw  37395  elaa2lem  37397  etransclem1  37399  etransclem12  37410  etransclem13  37411  etransclem17  37415  etransclem18  37416  etransclem21  37419  etransclem27  37425  etransclem31  37429  etransclem32  37430  etransclem33  37431  etransclem35  37433  etransclem46  37444  etransclem48  37446  iccpval  37695  vtxval  38025  gordval  38030  gsizval  38031  clintopval  38170  assintopval  38171  c0mgm  38239  c0mhm  38240  c0snmgmhm  38244  c0snmhm  38245  zrrnghm  38247  rngcvalALTV  38293  rngcval  38294  rngcidALTV  38323  zrinitorngc  38332  zrtermorngc  38333  ringcvalALTV  38339  ringcval  38340  funcringcsetcALTV2lem1  38368  ringcidALTV  38386  funcringcsetclem1ALTV  38391  zrtermoringc  38402  rhmsubcALTVlem3  38439  scmsuppss  38489  ply1mulgsum  38514  lincop  38533  lincext3  38581  lindslinindsimp1  38582  lindsrng01  38593  lincresunit2  38603  lincresunit3lem1  38604  islindeps2  38608  fdivmptfv  38689  refdivmptfv  38690  bigoval  38693  blenval  38715  digfval  38741
  Copyright terms: Public domain W3C validator