Theorem fveq12d 6679

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

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

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 2795

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 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-iota 6316  df-fv 6365

This theorem is referenced by:  nffvd  6684  wrecseq123  7950  tfrlem3a  8015  resixpfo  8502  cantnfval  9133  cantnfres  9142  fseqenlem1  9452  fseqenlem2  9453  dfac12lem1  9571  dfac12lem2  9572  dfac12r  9574  hsmexlem2  9851  ttukeylem3  9935  ttukey2g  9940  seq1  13385  expval  13434  lsw  13918  ccatfval  13927  swrdval  14007  splfv2a  14120  revval  14124  relexpsucnnr  14386  relexp1g  14387  seqshft  14446  climshft2  14941  fprodser  15305  imasval  16786  funcid  17142  funcco  17143  funcoppc  17147  funcres  17168  nati  17227  funcestrcsetclem7  17398  funcestrcsetclem9  17400  funcsetcestrclem7  17413  funcsetcestrclem9  17415  evlf2  17470  evlf1  17472  evlfcl  17474  uncf2  17489  hofcl  17511  yonedalem21  17525  yonedalem3a  17526  yonedalem4a  17527  yonedalem4b  17528  yonedalem22  17530  yonedalem3  17532  yonedainv  17533  p0val  17653  p1val  17654  gsumvalx  17888  gsumpropd  17890  gsumval2a  17897  gsumsgrpccat  18006  gsumccatOLD  18007  prdsinvlem  18210  mulgfval  18228  mulgfvalALT  18229  mulgval  18230  mulgnndir  18258  mulgpropd  18271  cntrval  18451  efgsf  18857  efgsval  18859  issrngd  19634  rlmval  19965  evlseu  20298  evlval  20310  selvffval  20331  selvval  20333  evls1fval  20484  evl1varpw  20526  chrval  20674  znval  20684  isphl  20774  isphld  20800  phlpropd  20801  cssval  20828  prdsinvgd2  20888  islindf  20958  madetsumid  21072  madufval  21248  smadiadetr  21286  decpmatval0  21374  chpmatfval  21440  isperf  21761  dfac14  22228  xkohmeo  22425  flffval  22599  fcfval  22643  cnextfval  22672  tsmsval2  22740  tsmspropd  22742  tngngp  23265  tngngp3  23267  isnlm  23286  sranlm  23295  cnncvsabsnegdemo  23771  ovoliunlem1  24105  ovoliunlem2  24106  limcfval  24472  dvfval  24497  dvreslem  24509  dvaddbr  24537  dvmulbr  24538  isuc1p  24736  ismon1p  24738  q1pval  24749  dgreq0  24857  vieta1lem2  24902  vieta1  24903  basellem5  25664  lgsval  25879  lgsneg  25899  israg  26485  iswlkon  27441  wlkres  27454  wlkp1lem3  27459  wlkp1lem6  27462  isclwlk  27556  iscrct  27573  iscycl  27574  eupth2eucrct  27998  dipfval  28481  splfv3  30634  cycpmco2lem5  30774  cycpmco2lem6  30775  extdgval  31046  lmatfval  31081  lmat22e11  31085  rrhval  31239  xrhval  31261  prodindf  31284  brae  31502  braew  31503  sitmval  31609  sseqval  31648  fibp1  31661  elprob  31669  signsvtn0  31842  signstfvneq0  31844  signstfveq0  31849  breprexplema  31903  breprexp  31906  circlevma  31915  circlemethhgt  31916  cvmliftlem5  32538  cvmliftlem7  32540  cvmliftlem10  32543  cvmliftlem13  32545  satefv  32663  mclsval  32812  rdgprc0  33040  dfrdg2  33042  bj-finsumval0  34569  rdgeqoa  34653  finxpeq2  34670  finxpreclem6  34679  finxpsuclem  34680  sdclem2  35019  ldualvsub  36293  ldualvsubval  36295  isopos  36318  polfvalN  37042  psubclsetN  37074  docaffvalN  38259  docafvalN  38260  djaffvalN  38271  djafvalN  38272  dihffval  38368  dihfval  38369  dochffval  38487  dochfval  38488  djhffval  38534  djhfval  38535  islpolN  38621  lcdfval  38726  lcdval  38727  lcdvsub  38755  lcdvsubval  38756  mapdffval  38764  mapdfval  38765  hdmap1fval  38934  hdmapfval  38965  hgmapfval  39024  hdmapglem7  39067  hlhilset  39072  0prjspnrel  39276  ismrc  39305  rmxfval  39508  rmyfval  39509  aomclem8  39668  hbt  39737  elmnc  39743  mncn0  39746  aaitgo  39769  mon1pid  39812  clsk1independent  40403  binomcxp  40696  limciccioolb  41909  limcicciooub  41925  ioccncflimc  42175  icocncflimc  42179  dvnprodlem2  42239  dvnprodlem3  42240  dirkercncflem3  42397  fourierdlem32  42431  etransclem32  42558  etransclem44  42570  etransclem46  42572  etransc  42575  ovnsubaddlem1  42859  ovnsubaddlem2  42860  ovnsubadd  42861  hoidmvlelem4  42887  hoidmvlelem5  42888  hspmbl  42918  vonioo  42971  vonicc  42974  afveq12d  43339  iccelpart  43600  nnsum3primesprm  43962  isomgreqve  43997  funcringcsetcALTV2lem7  44320  funcringcsetcALTV2lem9  44322  funcringcsetclem7ALTV  44343  funcringcsetclem9ALTV  44345