Theorem fveq12d 6868

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522

This theorem is referenced by:  nffvd  6873  fvmpopr2d  7554  tfrlem3a  8348  resixpfo  8912  cantnfval  9628  cantnfres  9637  fseqenlem1  9984  fseqenlem2  9985  dfac12lem1  10104  dfac12lem2  10105  dfac12r  10107  hsmexlem2  10387  ttukeylem3  10471  ttukey2g  10476  seq1  13986  expval  14035  lsw  14536  ccatfval  14545  swrdval  14615  splfv2a  14728  revval  14732  relexpsucnnr  14998  relexp1g  14999  seqshft  15058  climshft2  15555  fprodser  15922  imasval  17481  funcid  17839  funcco  17840  funcoppc  17844  funcres  17865  nati  17927  funcestrcsetclem7  18114  funcestrcsetclem9  18116  funcsetcestrclem7  18129  funcsetcestrclem9  18131  evlf2  18186  evlf1  18188  evlfcl  18190  uncf2  18205  hofcl  18227  yonedalem21  18241  yonedalem3a  18242  yonedalem4a  18243  yonedalem4b  18244  yonedalem22  18246  yonedalem3  18248  yonedainv  18249  p0val  18393  p1val  18394  gsumvalx  18610  gsumpropd  18612  gsumval2a  18619  gsumsgrpccat  18774  prdsinvlem  18988  mulgfval  19008  mulgfvalALT  19009  mulgval  19010  mulgnndir  19042  mulgpropd  19055  cntrval  19258  efgsf  19666  efgsval  19668  issrngd  20771  rlmval  21105  chrval  21440  znval  21452  isphl  21544  isphld  21570  phlpropd  21571  cssval  21598  prdsinvgd2  21658  islindf  21728  evlseu  21997  evlval  22009  selvffval  22027  selvval  22029  evls1fval  22213  evl1varpw  22255  madetsumid  22355  madufval  22531  smadiadetr  22569  decpmatval0  22658  chpmatfval  22724  isperf  23045  dfac14  23512  xkohmeo  23709  flffval  23883  fcfval  23927  cnextfval  23956  tsmsval2  24024  tsmspropd  24026  tngngp  24549  tngngp3  24551  isnlm  24570  sranlm  24579  cnncvsabsnegdemo  25072  ovoliunlem1  25410  ovoliunlem2  25411  limcfval  25780  dvfval  25805  dvreslem  25817  dvaddbr  25847  dvmulbr  25848  dvmulbrOLD  25849  isuc1p  26053  ismon1p  26055  mon1pid  26066  q1pval  26067  dgreq0  26178  vieta1lem2  26226  vieta1  26227  basellem5  27002  lgsval  27219  lgsneg  27239  seqseq123d  28187  israg  28631  iswlkon  29592  wlkres  29605  wlkp1lem3  29610  wlkp1lem6  29613  isclwlk  29710  iscrct  29727  iscycl  29728  eupth2eucrct  30153  dipfval  30638  prodindf  32793  splfv3  32887  cycpmco2lem5  33094  cycpmco2lem6  33095  idlsrgval  33481  m1pmeq  33559  extdgval  33656  fldextrspundgle  33680  minplyval  33702  constrcon  33771  2sqr3minply  33777  lmatfval  33811  lmat22e11  33815  rrhval  33993  xrhval  34015  brae  34238  braew  34239  sitmval  34347  sseqval  34386  fibp1  34399  elprob  34407  signsvtn0  34568  signstfvneq0  34570  signstfveq0  34575  breprexplema  34628  breprexp  34631  circlevma  34640  circlemethhgt  34641  cvmliftlem5  35283  cvmliftlem7  35285  cvmliftlem10  35288  cvmliftlem13  35290  satefv  35408  mclsval  35557  rdgprc0  35788  dfrdg2  35790  bj-finsumval0  37280  rdgeqoa  37365  finxpeq2  37382  finxpreclem6  37391  finxpsuclem  37392  sdclem2  37743  ldualvsub  39155  ldualvsubval  39157  isopos  39180  polfvalN  39905  psubclsetN  39937  docaffvalN  41122  docafvalN  41123  djaffvalN  41134  djafvalN  41135  dihffval  41231  dihfval  41232  dochffval  41350  dochfval  41351  djhffval  41397  djhfval  41398  islpolN  41484  lcdfval  41589  lcdval  41590  lcdvsub  41618  lcdvsubval  41619  mapdffval  41627  mapdfval  41628  hdmap1fval  41797  hdmapfval  41828  hgmapfval  41887  hdmapglem7  41930  hlhilset  41935  aks6d1c1p1  42102  evlselv  42582  0prjspnrel  42622  ismrc  42696  rmxfval  42899  rmyfval  42900  aomclem8  43057  hbt  43126  elmnc  43132  mncn0  43135  aaitgo  43158  clsk1independent  44042  binomcxp  44353  limciccioolb  45626  limcicciooub  45642  ioccncflimc  45890  icocncflimc  45894  dvnprodlem2  45952  dvnprodlem3  45953  dirkercncflem3  46110  fourierdlem32  46144  etransclem32  46271  etransclem44  46283  etransclem46  46285  etransc  46288  ovnsubaddlem1  46575  ovnsubaddlem2  46576  ovnsubadd  46577  hoidmvlelem4  46603  hoidmvlelem5  46604  hspmbl  46634  vonioo  46687  vonicc  46690  afveq12d  47138  iccelpart  47438  nnsum3primesprm  47795  funcringcsetcALTV2lem7  48288  funcringcsetcALTV2lem9  48290  funcringcsetclem7ALTV  48311  funcringcsetclem9ALTV  48313  cofu1a  49087  cofu2a  49088  cofid1  49107  cofid2  49108  uptr2  49214  swapfida  49273  cofuswapf2  49288  fuco21  49329  fuco23  49334  fucoid  49341  opf2  49399  oppfdiag1  49407  oppfdiag  49409  termolmd  49663