Theorem fveq12d 6109

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

Syntax hints:   → wi 4   = wceq 1475  ‘cfv 5804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812

This theorem is referenced by:  nffvd  6112  fvsng  6352  wrecseq123  7295  tfrlem3a  7360  resixpfo  7832  cantnfval  8448  cantnfres  8457  fseqenlem1  8730  fseqenlem2  8731  dfac12lem1  8848  dfac12lem2  8849  dfac12r  8851  hsmexlem2  9132  ttukeylem3  9216  ttukey2g  9221  seq1  12676  expval  12724  lsw  13204  ccatfval  13211  swrdval  13269  splfv2a  13358  revval  13360  relexpsucnnr  13613  relexp1g  13614  seqshft  13673  climshft2  14161  fprodser  14518  imasval  15994  funcid  16353  funcco  16354  funcoppc  16358  funcres  16379  nati  16438  funcestrcsetclem7  16609  funcestrcsetclem9  16611  funcsetcestrclem7  16624  funcsetcestrclem9  16626  evlf2  16681  evlf1  16683  evlfcl  16685  uncf2  16700  hofcl  16722  yonedalem21  16736  yonedalem3a  16737  yonedalem4a  16738  yonedalem4b  16739  yonedalem22  16741  yonedalem3  16743  yonedainv  16744  p0val  16864  p1val  16865  gsumvalx  17093  gsumpropd  17095  gsumval2a  17102  gsumccat  17201  prdsinvlem  17347  mulgfval  17365  mulgval  17366  mulgnndir  17392  mulgnndirOLD  17393  mulgpropd  17407  cntrval  17575  efgsf  17965  efgsval  17967  issrngd  18684  rlmval  19012  evlseu  19337  evlval  19345  evls1fval  19505  evl1varpw  19546  chrval  19692  znval  19702  isphl  19792  isphld  19818  phlpropd  19819  cssval  19845  prdsinvgd2  19905  islindf  19970  madetsumid  20086  madufval  20262  smadiadetr  20300  decpmatval0  20388  chpmatfval  20454  isperf  20765  dfac14  21231  xkohmeo  21428  flffval  21603  fcfval  21647  cnextfval  21676  tsmsval2  21743  tsmspropd  21745  tngngp  22268  tngngp3  22270  isnlm  22289  sranlm  22298  cnncvsabsnegdemo  22773  ovoliunlem1  23077  ovoliunlem2  23078  limcfval  23442  dvfval  23467  dvreslem  23479  dvaddbr  23507  dvmulbr  23508  isuc1p  23704  ismon1p  23706  q1pval  23717  dgreq0  23825  vieta1lem2  23870  vieta1  23871  basellem5  24611  lgsval  24826  lgsneg  24846  israg  25392  iscgra  25501  iswlkon  26062  iscrct  26152  iscycl  26153  isclwlk0  26282  dipfval  26941  lmatfval  29208  lmat22e11  29212  rrhval  29368  xrhval  29390  brae  29631  braew  29632  sitmval  29738  sseqval  29777  fibp1  29790  elprob  29798  signsvtn0  29973  signstfvneq0  29975  signstfveq0  29980  cvmliftlem5  30525  cvmliftlem7  30527  cvmliftlem10  30530  cvmliftlem13  30532  mclsval  30714  rdgprc0  30943  dfrdg2  30945  bj-finsumval0  32324  rdgeqoa  32394  finxpeq2  32400  finxpreclem6  32409  finxpsuclem  32410  sdclem2  32708  ldualvsub  33460  ldualvsubval  33462  isopos  33485  polfvalN  34208  psubclsetN  34240  docaffvalN  35428  docafvalN  35429  djaffvalN  35440  djafvalN  35441  dihffval  35537  dihfval  35538  dochffval  35656  dochfval  35657  djhffval  35703  djhfval  35704  islpolN  35790  lcdfval  35895  lcdval  35896  lcdvsub  35924  lcdvsubval  35925  mapdffval  35933  mapdfval  35934  hdmap1fval  36104  hdmapfval  36137  hgmapfval  36196  hdmapglem7  36239  hlhilset  36244  ismrc  36282  rmxfval  36486  rmyfval  36487  aomclem8  36649  hbt  36719  elmnc  36725  mncn0  36728  aaitgo  36751  mon1pid  36802  clsk1independent  37364  binomcxp  37578  limciccioolb  38688  limcicciooub  38704  ioccncflimc  38771  icocncflimc  38775  dvnprodlem2  38837  dvnprodlem3  38838  dirkercncflem3  38998  fourierdlem32  39032  etransclem32  39159  etransclem44  39171  etransclem46  39173  etransc  39176  ovnsubaddlem1  39460  ovnsubaddlem2  39461  ovnsubadd  39462  hoidmvlelem4  39488  hoidmvlelem5  39489  hspmbl  39519  vonioo  39573  vonicc  39576  afveq12d  39862  iccelpart  39971  nnsum3primesprm  40206  iswlkOn  40865  1wlkres  40879  1wlkp1lem3  40884  1wlkp1lem6  40887  isclWlk  40979  isCrct  40996  isCycl  40997  eupth2eucrct  41385  funcringcsetcALTV2lem7  41834  funcringcsetcALTV2lem9  41836  funcringcsetclem7ALTV  41857  funcringcsetclem9ALTV  41859