Theorem fveq12d 6677

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 6672	. 2 ⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐴))
3		fveq12d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4	3	fveq2d 6674	. 2 ⊢ (𝜑 → (𝐺‘𝐴) = (𝐺‘𝐵))
5	2, 4	eqtrd 2856	1 ⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐵))

Syntax hints:   → wi 4   = wceq 1537  ‘cfv 6355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363

This theorem is referenced by:  nffvd  6682  wrecseq123  7948  tfrlem3a  8013  resixpfo  8500  cantnfval  9131  cantnfres  9140  fseqenlem1  9450  fseqenlem2  9451  dfac12lem1  9569  dfac12lem2  9570  dfac12r  9572  hsmexlem2  9849  ttukeylem3  9933  ttukey2g  9938  seq1  13383  expval  13432  lsw  13916  ccatfval  13925  swrdval  14005  splfv2a  14118  revval  14122  relexpsucnnr  14384  relexp1g  14385  seqshft  14444  climshft2  14939  fprodser  15303  imasval  16784  funcid  17140  funcco  17141  funcoppc  17145  funcres  17166  nati  17225  funcestrcsetclem7  17396  funcestrcsetclem9  17398  funcsetcestrclem7  17411  funcsetcestrclem9  17413  evlf2  17468  evlf1  17470  evlfcl  17472  uncf2  17487  hofcl  17509  yonedalem21  17523  yonedalem3a  17524  yonedalem4a  17525  yonedalem4b  17526  yonedalem22  17528  yonedalem3  17530  yonedainv  17531  p0val  17651  p1val  17652  gsumvalx  17886  gsumpropd  17888  gsumval2a  17895  gsumsgrpccat  18004  gsumccatOLD  18005  prdsinvlem  18208  mulgfval  18226  mulgfvalALT  18227  mulgval  18228  mulgnndir  18256  mulgpropd  18269  cntrval  18449  efgsf  18855  efgsval  18857  issrngd  19632  rlmval  19963  evlseu  20296  evlval  20308  selvffval  20329  selvval  20331  evls1fval  20482  evl1varpw  20524  chrval  20672  znval  20682  isphl  20772  isphld  20798  phlpropd  20799  cssval  20826  prdsinvgd2  20886  islindf  20956  madetsumid  21070  madufval  21246  smadiadetr  21284  decpmatval0  21372  chpmatfval  21438  isperf  21759  dfac14  22226  xkohmeo  22423  flffval  22597  fcfval  22641  cnextfval  22670  tsmsval2  22738  tsmspropd  22740  tngngp  23263  tngngp3  23265  isnlm  23284  sranlm  23293  cnncvsabsnegdemo  23769  ovoliunlem1  24103  ovoliunlem2  24104  limcfval  24470  dvfval  24495  dvreslem  24507  dvaddbr  24535  dvmulbr  24536  isuc1p  24734  ismon1p  24736  q1pval  24747  dgreq0  24855  vieta1lem2  24900  vieta1  24901  basellem5  25662  lgsval  25877  lgsneg  25897  israg  26483  iswlkon  27439  wlkres  27452  wlkp1lem3  27457  wlkp1lem6  27460  isclwlk  27554  iscrct  27571  iscycl  27572  eupth2eucrct  27996  dipfval  28479  splfv3  30632  cycpmco2lem5  30772  cycpmco2lem6  30773  extdgval  31044  lmatfval  31079  lmat22e11  31083  rrhval  31237  xrhval  31259  prodindf  31282  brae  31500  braew  31501  sitmval  31607  sseqval  31646  fibp1  31659  elprob  31667  signsvtn0  31840  signstfvneq0  31842  signstfveq0  31847  breprexplema  31901  breprexp  31904  circlevma  31913  circlemethhgt  31914  cvmliftlem5  32536  cvmliftlem7  32538  cvmliftlem10  32541  cvmliftlem13  32543  satefv  32661  mclsval  32810  rdgprc0  33038  dfrdg2  33040  bj-finsumval0  34570  rdgeqoa  34654  finxpeq2  34671  finxpreclem6  34680  finxpsuclem  34681  sdclem2  35032  ldualvsub  36306  ldualvsubval  36308  isopos  36331  polfvalN  37055  psubclsetN  37087  docaffvalN  38272  docafvalN  38273  djaffvalN  38284  djafvalN  38285  dihffval  38381  dihfval  38382  dochffval  38500  dochfval  38501  djhffval  38547  djhfval  38548  islpolN  38634  lcdfval  38739  lcdval  38740  lcdvsub  38768  lcdvsubval  38769  mapdffval  38777  mapdfval  38778  hdmap1fval  38947  hdmapfval  38978  hgmapfval  39037  hdmapglem7  39080  hlhilset  39085  0prjspnrel  39289  ismrc  39318  rmxfval  39521  rmyfval  39522  aomclem8  39681  hbt  39750  elmnc  39756  mncn0  39759  aaitgo  39782  mon1pid  39825  clsk1independent  40416  binomcxp  40709  limciccioolb  41922  limcicciooub  41938  ioccncflimc  42188  icocncflimc  42192  dvnprodlem2  42252  dvnprodlem3  42253  dirkercncflem3  42410  fourierdlem32  42444  etransclem32  42571  etransclem44  42583  etransclem46  42585  etransc  42588  ovnsubaddlem1  42872  ovnsubaddlem2  42873  ovnsubadd  42874  hoidmvlelem4  42900  hoidmvlelem5  42901  hspmbl  42931  vonioo  42984  vonicc  42987  afveq12d  43352  iccelpart  43613  nnsum3primesprm  43975  isomgreqve  44010  funcringcsetcALTV2lem7  44333  funcringcsetcALTV2lem9  44335  funcringcsetclem7ALTV  44356  funcringcsetclem9ALTV  44358