Theorem fveq12d 6849

Description: Equality deduction for function value. (Contributed by FL, 22-Dec-2008.)

Hypotheses

Ref	Expression
fveq12d.1	⊢ (𝜑 → 𝐹 = 𝐺)
fveq12d.2	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
fveq12d	⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐵))

Proof of Theorem fveq12d

Step	Hyp	Ref	Expression
1		fveq12d.1	. . 3 ⊢ (𝜑 → 𝐹 = 𝐺)
2	1	fveq1d 6844	. 2 ⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐴))
3		fveq12d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4	3	fveq2d 6846	. 2 ⊢ (𝜑 → (𝐺‘𝐴) = (𝐺‘𝐵))
5	2, 4	eqtrd 2772	1 ⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐵))

Syntax hints:   → wi 4   = wceq 1542  ‘cfv 6500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508

This theorem is referenced by:  nffvd  6854  fvmpopr2d  7530  tfrlem3a  8318  resixpfo  8886  cantnfval  9589  cantnfres  9598  fseqenlem1  9946  fseqenlem2  9947  dfac12lem1  10066  dfac12lem2  10067  dfac12r  10069  hsmexlem2  10349  ttukeylem3  10433  ttukey2g  10438  seq1  13949  expval  13998  lsw  14499  ccatfval  14508  swrdval  14579  splfv2a  14691  revval  14695  relexpsucnnr  14960  relexp1g  14961  seqshft  15020  climshft2  15517  fprodser  15884  imasval  17444  funcid  17806  funcco  17807  funcoppc  17811  funcres  17832  nati  17894  funcestrcsetclem7  18081  funcestrcsetclem9  18083  funcsetcestrclem7  18096  funcsetcestrclem9  18098  evlf2  18153  evlf1  18155  evlfcl  18157  uncf2  18172  hofcl  18194  yonedalem21  18208  yonedalem3a  18209  yonedalem4a  18210  yonedalem4b  18211  yonedalem22  18213  yonedalem3  18215  yonedainv  18216  p0val  18360  p1val  18361  gsumvalx  18613  gsumpropd  18615  gsumval2a  18622  gsumsgrpccat  18777  prdsinvlem  18991  mulgfval  19011  mulgfvalALT  19012  mulgval  19013  mulgnndir  19045  mulgpropd  19058  cntrval  19260  efgsf  19670  efgsval  19672  issrngd  20800  rlmval  21155  chrval  21490  znval  21502  isphl  21595  isphld  21621  phlpropd  21622  cssval  21649  prdsinvgd2  21709  islindf  21779  evlseu  22050  evlval  22067  selvffval  22088  selvval  22090  evls1fval  22275  evl1varpw  22317  madetsumid  22417  madufval  22593  smadiadetr  22631  decpmatval0  22720  chpmatfval  22786  isperf  23107  dfac14  23574  xkohmeo  23771  flffval  23945  fcfval  23989  cnextfval  24018  tsmsval2  24086  tsmspropd  24088  tngngp  24610  tngngp3  24612  isnlm  24631  sranlm  24640  cnncvsabsnegdemo  25133  ovoliunlem1  25471  ovoliunlem2  25472  limcfval  25841  dvfval  25866  dvreslem  25878  dvaddbr  25908  dvmulbr  25909  dvmulbrOLD  25910  isuc1p  26114  ismon1p  26116  mon1pid  26127  q1pval  26128  dgreq0  26239  vieta1lem2  26287  vieta1  26288  basellem5  27063  lgsval  27280  lgsneg  27300  seqseq123d  28294  israg  28781  iswlkon  29741  wlkres  29754  wlkp1lem3  29759  wlkp1lem6  29762  isclwlk  29858  iscrct  29875  iscycl  29876  eupth2eucrct  30304  dipfval  30789  prodindf  32954  splfv3  33050  cycpmco2lem5  33223  cycpmco2lem6  33224  idlsrgval  33595  m1pmeq  33677  mplvrpmfgalem  33720  mplvrpmga  33721  mplvrpmmhm  33722  mplvrpmrhm  33723  issply  33737  esplyval  33738  esplyind  33751  vieta  33756  extdgval  33830  fldextrspundgle  33855  minplyval  33882  constrcon  33951  2sqr3minply  33957  lmatfval  33991  lmat22e11  33995  rrhval  34173  xrhval  34195  brae  34418  braew  34419  sitmval  34526  sseqval  34565  fibp1  34578  elprob  34586  signsvtn0  34747  signstfvneq0  34749  signstfveq0  34754  breprexplema  34807  breprexp  34810  circlevma  34819  circlemethhgt  34820  cvmliftlem5  35502  cvmliftlem7  35504  cvmliftlem10  35507  cvmliftlem13  35509  satefv  35627  mclsval  35776  rdgprc0  36004  dfrdg2  36006  bj-finsumval0  37537  rdgeqoa  37622  finxpeq2  37639  finxpreclem6  37648  finxpsuclem  37649  sdclem2  37990  ldualvsub  39528  ldualvsubval  39530  isopos  39553  polfvalN  40277  psubclsetN  40309  docaffvalN  41494  docafvalN  41495  djaffvalN  41506  djafvalN  41507  dihffval  41603  dihfval  41604  dochffval  41722  dochfval  41723  djhffval  41769  djhfval  41770  islpolN  41856  lcdfval  41961  lcdval  41962  lcdvsub  41990  lcdvsubval  41991  mapdffval  41999  mapdfval  42000  hdmap1fval  42169  hdmapfval  42200  hgmapfval  42259  hdmapglem7  42302  hlhilset  42307  aks6d1c1p1  42474  evlselv  42942  0prjspnrel  42982  ismrc  43055  rmxfval  43258  rmyfval  43259  aomclem8  43415  hbt  43484  elmnc  43490  mncn0  43493  aaitgo  43516  clsk1independent  44399  binomcxp  44710  limciccioolb  45978  limcicciooub  45992  ioccncflimc  46240  icocncflimc  46244  dvnprodlem2  46302  dvnprodlem3  46303  dirkercncflem3  46460  fourierdlem32  46494  etransclem32  46621  etransclem44  46633  etransclem46  46635  etransc  46638  ovnsubaddlem1  46925  ovnsubaddlem2  46926  ovnsubadd  46927  hoidmvlelem4  46953  hoidmvlelem5  46954  hspmbl  46984  vonioo  47037  vonicc  47040  afveq12d  47490  iccelpart  47790  nnsum3primesprm  48147  funcringcsetcALTV2lem7  48653  funcringcsetcALTV2lem9  48655  funcringcsetclem7ALTV  48676  funcringcsetclem9ALTV  48678  cofu1a  49450  cofu2a  49451  cofid1  49470  cofid2  49471  uptr2  49577  swapfida  49636  cofuswapf2  49651  fuco21  49692  fuco23  49697  fucoid  49704  opf2  49762  oppfdiag1  49770  oppfdiag  49772  termolmd  50026