Theorem fveq12d 6847

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

Syntax hints:   → wi 4   = wceq 1542  ‘cfv 6498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506

This theorem is referenced by:  nffvd  6852  fvmpopr2d  7529  tfrlem3a  8316  resixpfo  8884  cantnfval  9589  cantnfres  9598  fseqenlem1  9946  fseqenlem2  9947  dfac12lem1  10066  dfac12lem2  10067  dfac12r  10069  hsmexlem2  10349  ttukeylem3  10433  ttukey2g  10438  seq1  13976  expval  14025  lsw  14526  ccatfval  14535  swrdval  14606  splfv2a  14718  revval  14722  relexpsucnnr  14987  relexp1g  14988  seqshft  15047  climshft2  15544  fprodser  15914  imasval  17475  funcid  17837  funcco  17838  funcoppc  17842  funcres  17863  nati  17925  funcestrcsetclem7  18112  funcestrcsetclem9  18114  funcsetcestrclem7  18127  funcsetcestrclem9  18129  evlf2  18184  evlf1  18186  evlfcl  18188  uncf2  18203  hofcl  18225  yonedalem21  18239  yonedalem3a  18240  yonedalem4a  18241  yonedalem4b  18242  yonedalem22  18244  yonedalem3  18246  yonedainv  18247  p0val  18391  p1val  18392  gsumvalx  18644  gsumpropd  18646  gsumval2a  18653  gsumsgrpccat  18808  prdsinvlem  19025  mulgfval  19045  mulgfvalALT  19046  mulgval  19047  mulgnndir  19079  mulgpropd  19092  cntrval  19294  efgsf  19704  efgsval  19706  issrngd  20832  rlmval  21186  chrval  21503  znval  21515  isphl  21608  isphld  21634  phlpropd  21635  cssval  21662  prdsinvgd2  21722  islindf  21792  evlseu  22061  evlval  22078  selvffval  22099  selvval  22101  evls1fval  22284  evl1varpw  22326  madetsumid  22426  madufval  22602  smadiadetr  22640  decpmatval0  22729  chpmatfval  22795  isperf  23116  dfac14  23583  xkohmeo  23780  flffval  23954  fcfval  23998  cnextfval  24027  tsmsval2  24095  tsmspropd  24097  tngngp  24619  tngngp3  24621  isnlm  24640  sranlm  24649  cnncvsabsnegdemo  25132  ovoliunlem1  25469  ovoliunlem2  25470  limcfval  25839  dvfval  25864  dvreslem  25876  dvaddbr  25905  dvmulbr  25906  isuc1p  26106  ismon1p  26108  mon1pid  26119  q1pval  26120  dgreq0  26230  vieta1lem2  26277  vieta1  26278  basellem5  27048  lgsval  27264  lgsneg  27284  seqseq123d  28278  israg  28765  iswlkon  29724  wlkres  29737  wlkp1lem3  29742  wlkp1lem6  29745  isclwlk  29841  iscrct  29858  iscycl  29859  eupth2eucrct  30287  dipfval  30773  prodindf  32922  splfv3  33018  cycpmco2lem5  33191  cycpmco2lem6  33192  idlsrgval  33563  m1pmeq  33645  mplvrpmfgalem  33688  mplvrpmga  33689  mplvrpmmhm  33690  mplvrpmrhm  33691  issply  33705  esplyval  33706  esplyind  33719  vieta  33724  extdgval  33797  fldextrspundgle  33822  minplyval  33849  constrcon  33918  2sqr3minply  33924  lmatfval  33958  lmat22e11  33962  rrhval  34140  xrhval  34162  brae  34385  braew  34386  sitmval  34493  sseqval  34532  fibp1  34545  elprob  34553  signsvtn0  34714  signstfvneq0  34716  signstfveq0  34721  breprexplema  34774  breprexp  34777  circlevma  34786  circlemethhgt  34787  cvmliftlem5  35471  cvmliftlem7  35473  cvmliftlem10  35476  cvmliftlem13  35478  satefv  35596  mclsval  35745  rdgprc0  35973  dfrdg2  35975  bj-finsumval0  37599  rdgeqoa  37686  finxpeq2  37703  finxpreclem6  37712  finxpsuclem  37713  sdclem2  38063  ldualvsub  39601  ldualvsubval  39603  isopos  39626  polfvalN  40350  psubclsetN  40382  docaffvalN  41567  docafvalN  41568  djaffvalN  41579  djafvalN  41580  dihffval  41676  dihfval  41677  dochffval  41795  dochfval  41796  djhffval  41842  djhfval  41843  islpolN  41929  lcdfval  42034  lcdval  42035  lcdvsub  42063  lcdvsubval  42064  mapdffval  42072  mapdfval  42073  hdmap1fval  42242  hdmapfval  42273  hgmapfval  42332  hdmapglem7  42375  hlhilset  42380  aks6d1c1p1  42546  evlselv  43020  0prjspnrel  43060  ismrc  43133  rmxfval  43332  rmyfval  43333  aomclem8  43489  hbt  43558  elmnc  43564  mncn0  43567  aaitgo  43590  clsk1independent  44473  binomcxp  44784  limciccioolb  46051  limcicciooub  46065  ioccncflimc  46313  icocncflimc  46317  dvnprodlem2  46375  dvnprodlem3  46376  dirkercncflem3  46533  fourierdlem32  46567  etransclem32  46694  etransclem44  46706  etransclem46  46708  etransc  46711  ovnsubaddlem1  46998  ovnsubaddlem2  46999  ovnsubadd  47000  hoidmvlelem4  47026  hoidmvlelem5  47027  hspmbl  47057  vonioo  47110  vonicc  47113  afveq12d  47581  iccelpart  47893  nnsum3primesprm  48266  funcringcsetcALTV2lem7  48772  funcringcsetcALTV2lem9  48774  funcringcsetclem7ALTV  48795  funcringcsetclem9ALTV  48797  cofu1a  49569  cofu2a  49570  cofid1  49589  cofid2  49590  uptr2  49696  swapfida  49755  cofuswapf2  49770  fuco21  49811  fuco23  49816  fucoid  49823  opf2  49881  oppfdiag1  49889  oppfdiag  49891  termolmd  50145