Theorem fveq12d 6197

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

Syntax hints:   → wi 4   = wceq 1483  ‘cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896

This theorem is referenced by:  nffvd  6200  fvsng  6447  wrecseq123  7408  tfrlem3a  7473  resixpfo  7946  cantnfval  8565  cantnfres  8574  fseqenlem1  8847  fseqenlem2  8848  dfac12lem1  8965  dfac12lem2  8966  dfac12r  8968  hsmexlem2  9249  ttukeylem3  9333  ttukey2g  9338  seq1  12814  expval  12862  lsw  13351  ccatfval  13358  swrdval  13417  splfv2a  13507  revval  13509  relexpsucnnr  13765  relexp1g  13766  seqshft  13825  climshft2  14313  fprodser  14679  imasval  16171  funcid  16530  funcco  16531  funcoppc  16535  funcres  16556  nati  16615  funcestrcsetclem7  16786  funcestrcsetclem9  16788  funcsetcestrclem7  16801  funcsetcestrclem9  16803  evlf2  16858  evlf1  16860  evlfcl  16862  uncf2  16877  hofcl  16899  yonedalem21  16913  yonedalem3a  16914  yonedalem4a  16915  yonedalem4b  16916  yonedalem22  16918  yonedalem3  16920  yonedainv  16921  p0val  17041  p1val  17042  gsumvalx  17270  gsumpropd  17272  gsumval2a  17279  gsumccat  17378  prdsinvlem  17524  mulgfval  17542  mulgval  17543  mulgnndir  17569  mulgnndirOLD  17570  mulgpropd  17584  cntrval  17752  efgsf  18142  efgsval  18144  issrngd  18861  rlmval  19191  evlseu  19516  evlval  19524  evls1fval  19684  evl1varpw  19725  chrval  19873  znval  19883  isphl  19973  isphld  19999  phlpropd  20000  cssval  20026  prdsinvgd2  20086  islindf  20151  madetsumid  20267  madufval  20443  smadiadetr  20481  decpmatval0  20569  chpmatfval  20635  isperf  20955  dfac14  21421  xkohmeo  21618  flffval  21793  fcfval  21837  cnextfval  21866  tsmsval2  21933  tsmspropd  21935  tngngp  22458  tngngp3  22460  isnlm  22479  sranlm  22488  cnncvsabsnegdemo  22965  ovoliunlem1  23270  ovoliunlem2  23271  limcfval  23636  dvfval  23661  dvreslem  23673  dvaddbr  23701  dvmulbr  23702  isuc1p  23900  ismon1p  23902  q1pval  23913  dgreq0  24021  vieta1lem2  24066  vieta1  24067  basellem5  24811  lgsval  25026  lgsneg  25046  israg  25592  iscgra  25701  iswlkon  26553  wlkres  26567  wlkp1lem3  26572  wlkp1lem6  26575  isclwlk  26669  iscrct  26685  iscycl  26686  eupth2eucrct  27077  dipfval  27557  lmatfval  29880  lmat22e11  29884  rrhval  30040  xrhval  30062  prodindf  30085  brae  30304  braew  30305  sitmval  30411  sseqval  30450  fibp1  30463  elprob  30471  signsvtn0  30647  signstfvneq0  30649  signstfveq0  30654  breprexplema  30708  breprexp  30711  circlevma  30720  circlemethhgt  30721  cvmliftlem5  31271  cvmliftlem7  31273  cvmliftlem10  31276  cvmliftlem13  31278  mclsval  31460  rdgprc0  31699  dfrdg2  31701  bj-finsumval0  33147  rdgeqoa  33218  finxpeq2  33224  finxpreclem6  33233  finxpsuclem  33234  sdclem2  33538  ldualvsub  34442  ldualvsubval  34444  isopos  34467  polfvalN  35190  psubclsetN  35222  docaffvalN  36410  docafvalN  36411  djaffvalN  36422  djafvalN  36423  dihffval  36519  dihfval  36520  dochffval  36638  dochfval  36639  djhffval  36685  djhfval  36686  islpolN  36772  lcdfval  36877  lcdval  36878  lcdvsub  36906  lcdvsubval  36907  mapdffval  36915  mapdfval  36916  hdmap1fval  37086  hdmapfval  37119  hgmapfval  37178  hdmapglem7  37221  hlhilset  37226  ismrc  37264  rmxfval  37468  rmyfval  37469  aomclem8  37631  hbt  37700  elmnc  37706  mncn0  37709  aaitgo  37732  mon1pid  37783  clsk1independent  38344  binomcxp  38556  limciccioolb  39853  limcicciooub  39869  ioccncflimc  40098  icocncflimc  40102  dvnprodlem2  40162  dvnprodlem3  40163  dirkercncflem3  40322  fourierdlem32  40356  etransclem32  40483  etransclem44  40495  etransclem46  40497  etransc  40500  ovnsubaddlem1  40784  ovnsubaddlem2  40785  ovnsubadd  40786  hoidmvlelem4  40812  hoidmvlelem5  40813  hspmbl  40843  vonioo  40896  vonicc  40899  afveq12d  41213  iccelpart  41369  nnsum3primesprm  41678  funcringcsetcALTV2lem7  42042  funcringcsetcALTV2lem9  42044  funcringcsetclem7ALTV  42065  funcringcsetclem9ALTV  42067