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

Theorem fvmptd 5955
Description: Deduction version of fvmpt 5950. (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 5868 . 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 3462 . . . 4  |-  ( ph  ->  [_ A  /  x ]_ B  =  C
)
6 fvmptd.4 . . . 4  |-  ( ph  ->  C  e.  V )
75, 6eqeltrd 2555 . . 3  |-  ( ph  ->  [_ A  /  x ]_ B  e.  V
)
8 eqid 2467 . . . 4  |-  ( x  e.  D  |->  B )  =  ( x  e.  D  |->  B )
98fvmpts 5952 . . 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 2512 1  |-  ( ph  ->  ( F `  A
)  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1379    e. wcel 1767   [_csb 3435    |-> cmpt 4505   ` cfv 5588
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-iota 5551  df-fun 5590  df-fv 5596
This theorem is referenced by:  fvmptdv2  5963  mpt2curryvald  6999  ttukeylem3  8891  ccatval1  12560  ccatval2  12561  repswsymb  12709  prdsvscafval  14735  mrcval  14865  cidval  14932  subcid  15074  idfu2nd  15104  resf2nd  15122  fuccoval  15190  fucid  15198  homaval  15216  idaval  15243  setcval  15262  setcid  15271  catcval  15281  catcid  15288  prf1  15327  prf2  15329  curf1  15352  curf11  15353  curf2val  15357  hofval  15379  hof2  15384  yonval  15388  yonedalem4a  15402  frmdval  15851  vrmdval  15857  pmtrdifwrdellem3  16314  gexval  16404  pj1val  16519  dpjval  16907  sraval  17622  opsrval  17938  cply1mul  18134  cply1coe0  18140  cply1coe0bi  18141  gsummoncoe1  18145  evls1sca  18159  frlmphl  18607  mat1rhmval  18776  scmatrhmval  18824  mvmulfv  18841  mavmulfv  18843  mdetuni0  18918  mat2pmatval  19020  m2cpm  19037  cpm2mval  19046  m2cpminvid2lem  19050  decpmatid  19066  decpmatmullem  19067  pmatcollpw2lem  19073  monmatcollpw  19075  pmatcollpw3fi1lem1  19082  pm2mpfval  19092  mply1topmatval  19100  mp2pm2mplem1  19102  mp2pm2mplem4  19105  pm2mpmhmlem2  19115  chpmatval  19127  chfacfscmul0  19154  chfacfscmulgsum  19156  chfacfpmmul0  19158  chfacfpmmulgsum  19160  cpmidpmatlem1  19166  lmfval  19527  kgenval  19799  ptval  19834  fcfval  20297  cnextfval  20325  ustval  20468  utopval  20498  ustuqtoplem  20505  utopsnneiplem  20513  tusval  20532  blfvalps  20649  tmsval  20747  metuvalOLD  20815  metuval  20816  caufval  21477  rrxmvallem  21594  rrxmval  21595  taylpval  22524  logexprlim  23256  dchrval  23265  dchr1  23288  mirval  23777  mirfv  23778  israg  23810  perpln1  23823  perpln2  23824  isperp  23825  midf  23847  ismidb  23849  lmif  23856  islmib  23858  edgval  24043  wlkiswwlk2lem2  24396  clwlkisclwwlklem2fv1  24486  clwlkisclwwlklem2fv2  24487  sgnsval  27408  metidval  27533  pstmval  27538  qqhvval  27628  indv  27694  indval  27695  indfval  27698  esummulc1  27755  esumcvg  27760  ofcval  27766  sigagenval  27808  measinb  27860  omsval  27932  omsfval  27933  sitgfval  27951  eulerpartlemsv1  27963  eulerpartlems  27967  eulerpartlemgvv  27983  fibp1  28008  totprobd  28033  probmeasb  28037  cndprobval  28040  dstrvprob  28078  dstfrvinc  28083  dstfrvclim1  28084  ballotlemfval  28096  ballotlemsv  28116  gsumnunsn  28161  signsply0  28176  signstfval  28189  afsval  28219  lgamgulmlem2  28240  lgamcvglem  28250  cvmliftlem9  28406  relexp0  28555  relexpsucr  28556  rtrclreclem.subset  28571  rtrclreclem.min  28573  dfrtrcl2  28574  mblfinlem2  29657  areacirc  29717  itgpowd  30815  hashnzfzclim  30855  fmuldfeqlem1  31160  clim1fr1  31171  climrec  31173  climexp  31175  climneg  31180  mullimcf  31193  divcnvg  31197  sumnnodd  31200  cncfshift  31240  icccncfext  31254  cncfioobdlem  31263  dvsinax  31269  fperdvper  31276  dvcosax  31284  ioodvbdlimc1lem1  31289  ioodvbdlimc1lem2  31290  ioodvbdlimc2lem  31292  itgsinexp  31300  itgcoscmulx  31315  itgsincmulx  31320  itgsubsticclem  31321  itgsubsticc  31322  itgiccshift  31326  itgsbtaddcnst  31328  stoweidlem7  31335  stoweidlem17  31345  stoweidlem32  31360  stoweidlem34  31362  wallispilem4  31396  wallispilem5  31397  wallispi  31398  wallispi2lem1  31399  wallispi2lem2  31400  wallispi2  31401  stirlinglem1  31402  stirlinglem2  31403  stirlinglem3  31404  stirlinglem4  31405  stirlinglem5  31406  stirlinglem7  31408  stirlinglem8  31409  stirlinglem10  31411  stirlinglem11  31412  stirlinglem12  31413  stirlinglem13  31414  stirlinglem14  31415  stirlinglem15  31416  dirkerval2  31422  dirkeritg  31430  dirkercncflem2  31432  dirkercncflem4  31434  fourierdlem7  31442  fourierdlem13  31448  fourierdlem14  31449  fourierdlem16  31451  fourierdlem18  31453  fourierdlem19  31454  fourierdlem21  31456  fourierdlem22  31457  fourierdlem26  31461  fourierdlem37  31472  fourierdlem39  31474  fourierdlem41  31476  fourierdlem45  31480  fourierdlem48  31483  fourierdlem49  31484  fourierdlem50  31485  fourierdlem51  31486  fourierdlem53  31488  fourierdlem62  31497  fourierdlem63  31498  fourierdlem65  31500  fourierdlem73  31508  fourierdlem74  31509  fourierdlem75  31510  fourierdlem76  31511  fourierdlem78  31513  fourierdlem79  31514  fourierdlem81  31516  fourierdlem82  31517  fourierdlem83  31518  fourierdlem84  31519  fourierdlem88  31523  fourierdlem89  31524  fourierdlem90  31525  fourierdlem91  31526  fourierdlem92  31527  fourierdlem93  31528  fourierdlem97  31532  fourierdlem101  31536  fourierdlem103  31538  fourierdlem104  31539  fourierdlem111  31546  fourierdlem112  31547  fouriersw  31560  vtxval  31878  gordval  31883  gsizval  31884  clintopval  31984  assintopval  31985  scmsuppss  32064  ply1mulgsum  32089  lincop  32108  lincext3  32156  lindslinindsimp1  32157  lindsrng01  32168  lincresunit2  32178  lincresunit3lem1  32179  islindeps2  32183  bj-finsumval0  33753  cdleme31fv2  35207  tendopl2  35591  tendoi2  35609  erngplus2  35618  erngplus2-rN  35626  hlhilset  36752
  Copyright terms: Public domain W3C validator