Theorem fveq12d 6913

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

Syntax hints:   → wi 4   = wceq 1540  ‘cfv 6561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569

This theorem is referenced by:  nffvd  6918  fvmpopr2d  7595  wrecseq123OLD  8340  tfrlem3a  8417  resixpfo  8976  cantnfval  9708  cantnfres  9717  fseqenlem1  10064  fseqenlem2  10065  dfac12lem1  10184  dfac12lem2  10185  dfac12r  10187  hsmexlem2  10467  ttukeylem3  10551  ttukey2g  10556  seq1  14055  expval  14104  lsw  14602  ccatfval  14611  swrdval  14681  splfv2a  14794  revval  14798  relexpsucnnr  15064  relexp1g  15065  seqshft  15124  climshft2  15618  fprodser  15985  imasval  17556  funcid  17915  funcco  17916  funcoppc  17920  funcres  17941  nati  18003  funcestrcsetclem7  18191  funcestrcsetclem9  18193  funcsetcestrclem7  18206  funcsetcestrclem9  18208  evlf2  18263  evlf1  18265  evlfcl  18267  uncf2  18282  hofcl  18304  yonedalem21  18318  yonedalem3a  18319  yonedalem4a  18320  yonedalem4b  18321  yonedalem22  18323  yonedalem3  18325  yonedainv  18326  p0val  18472  p1val  18473  gsumvalx  18689  gsumpropd  18691  gsumval2a  18698  gsumsgrpccat  18853  prdsinvlem  19067  mulgfval  19087  mulgfvalALT  19088  mulgval  19089  mulgnndir  19121  mulgpropd  19134  cntrval  19337  efgsf  19747  efgsval  19749  issrngd  20856  rlmval  21198  chrval  21538  znval  21550  isphl  21646  isphld  21672  phlpropd  21673  cssval  21700  prdsinvgd2  21762  islindf  21832  evlseu  22107  evlval  22119  selvffval  22137  selvval  22139  evls1fval  22323  evl1varpw  22365  madetsumid  22467  madufval  22643  smadiadetr  22681  decpmatval0  22770  chpmatfval  22836  isperf  23159  dfac14  23626  xkohmeo  23823  flffval  23997  fcfval  24041  cnextfval  24070  tsmsval2  24138  tsmspropd  24140  tngngp  24675  tngngp3  24677  isnlm  24696  sranlm  24705  cnncvsabsnegdemo  25199  ovoliunlem1  25537  ovoliunlem2  25538  limcfval  25907  dvfval  25932  dvreslem  25944  dvaddbr  25974  dvmulbr  25975  dvmulbrOLD  25976  isuc1p  26180  ismon1p  26182  mon1pid  26193  q1pval  26194  dgreq0  26305  vieta1lem2  26353  vieta1  26354  basellem5  27128  lgsval  27345  lgsneg  27365  seqseq123d  28292  israg  28705  iswlkon  29675  wlkres  29688  wlkp1lem3  29693  wlkp1lem6  29696  isclwlk  29793  iscrct  29810  iscycl  29811  eupth2eucrct  30236  dipfval  30721  prodindf  32848  splfv3  32943  cycpmco2lem5  33150  cycpmco2lem6  33151  idlsrgval  33531  m1pmeq  33608  extdgval  33705  fldextrspundgle  33728  minplyval  33748  2sqr3minply  33791  lmatfval  33813  lmat22e11  33817  rrhval  33997  xrhval  34019  brae  34242  braew  34243  sitmval  34351  sseqval  34390  fibp1  34403  elprob  34411  signsvtn0  34585  signstfvneq0  34587  signstfveq0  34592  breprexplema  34645  breprexp  34648  circlevma  34657  circlemethhgt  34658  cvmliftlem5  35294  cvmliftlem7  35296  cvmliftlem10  35299  cvmliftlem13  35301  satefv  35419  mclsval  35568  rdgprc0  35794  dfrdg2  35796  bj-finsumval0  37286  rdgeqoa  37371  finxpeq2  37388  finxpreclem6  37397  finxpsuclem  37398  sdclem2  37749  ldualvsub  39156  ldualvsubval  39158  isopos  39181  polfvalN  39906  psubclsetN  39938  docaffvalN  41123  docafvalN  41124  djaffvalN  41135  djafvalN  41136  dihffval  41232  dihfval  41233  dochffval  41351  dochfval  41352  djhffval  41398  djhfval  41399  islpolN  41485  lcdfval  41590  lcdval  41591  lcdvsub  41619  lcdvsubval  41620  mapdffval  41628  mapdfval  41629  hdmap1fval  41798  hdmapfval  41829  hgmapfval  41888  hdmapglem7  41931  hlhilset  41936  aks6d1c1p1  42108  evlselv  42597  0prjspnrel  42637  ismrc  42712  rmxfval  42915  rmyfval  42916  aomclem8  43073  hbt  43142  elmnc  43148  mncn0  43151  aaitgo  43174  clsk1independent  44059  binomcxp  44376  limciccioolb  45636  limcicciooub  45652  ioccncflimc  45900  icocncflimc  45904  dvnprodlem2  45962  dvnprodlem3  45963  dirkercncflem3  46120  fourierdlem32  46154  etransclem32  46281  etransclem44  46293  etransclem46  46295  etransc  46298  ovnsubaddlem1  46585  ovnsubaddlem2  46586  ovnsubadd  46587  hoidmvlelem4  46613  hoidmvlelem5  46614  hspmbl  46644  vonioo  46697  vonicc  46700  afveq12d  47145  iccelpart  47420  nnsum3primesprm  47777  funcringcsetcALTV2lem7  48212  funcringcsetcALTV2lem9  48214  funcringcsetclem7ALTV  48235  funcringcsetclem9ALTV  48237  swapfida  48986  cofuswapf2  48995  fuco21  49031  fuco23  49036  fucoid  49043