Theorem fveq12d 6829

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

Syntax hints:   → wi 4   = wceq 1541  ‘cfv 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-iota 6437  df-fv 6489

This theorem is referenced by:  nffvd  6834  fvmpopr2d  7508  tfrlem3a  8296  resixpfo  8860  cantnfval  9558  cantnfres  9567  fseqenlem1  9915  fseqenlem2  9916  dfac12lem1  10035  dfac12lem2  10036  dfac12r  10038  hsmexlem2  10318  ttukeylem3  10402  ttukey2g  10407  seq1  13921  expval  13970  lsw  14471  ccatfval  14480  swrdval  14551  splfv2a  14663  revval  14667  relexpsucnnr  14932  relexp1g  14933  seqshft  14992  climshft2  15489  fprodser  15856  imasval  17415  funcid  17777  funcco  17778  funcoppc  17782  funcres  17803  nati  17865  funcestrcsetclem7  18052  funcestrcsetclem9  18054  funcsetcestrclem7  18067  funcsetcestrclem9  18069  evlf2  18124  evlf1  18126  evlfcl  18128  uncf2  18143  hofcl  18165  yonedalem21  18179  yonedalem3a  18180  yonedalem4a  18181  yonedalem4b  18182  yonedalem22  18184  yonedalem3  18186  yonedainv  18187  p0val  18331  p1val  18332  gsumvalx  18584  gsumpropd  18586  gsumval2a  18593  gsumsgrpccat  18748  prdsinvlem  18962  mulgfval  18982  mulgfvalALT  18983  mulgval  18984  mulgnndir  19016  mulgpropd  19029  cntrval  19232  efgsf  19642  efgsval  19644  issrngd  20771  rlmval  21126  chrval  21461  znval  21473  isphl  21566  isphld  21592  phlpropd  21593  cssval  21620  prdsinvgd2  21680  islindf  21750  evlseu  22019  evlval  22031  selvffval  22049  selvval  22051  evls1fval  22235  evl1varpw  22277  madetsumid  22377  madufval  22553  smadiadetr  22591  decpmatval0  22680  chpmatfval  22746  isperf  23067  dfac14  23534  xkohmeo  23731  flffval  23905  fcfval  23949  cnextfval  23978  tsmsval2  24046  tsmspropd  24048  tngngp  24570  tngngp3  24572  isnlm  24591  sranlm  24600  cnncvsabsnegdemo  25093  ovoliunlem1  25431  ovoliunlem2  25432  limcfval  25801  dvfval  25826  dvreslem  25838  dvaddbr  25868  dvmulbr  25869  dvmulbrOLD  25870  isuc1p  26074  ismon1p  26076  mon1pid  26087  q1pval  26088  dgreq0  26199  vieta1lem2  26247  vieta1  26248  basellem5  27023  lgsval  27240  lgsneg  27260  seqseq123d  28217  israg  28676  iswlkon  29635  wlkres  29648  wlkp1lem3  29653  wlkp1lem6  29656  isclwlk  29752  iscrct  29769  iscycl  29770  eupth2eucrct  30195  dipfval  30680  prodindf  32842  splfv3  32937  cycpmco2lem5  33097  cycpmco2lem6  33098  idlsrgval  33466  m1pmeq  33545  mplvrpmfgalem  33572  mplvrpmga  33573  mplvrpmmhm  33574  mplvrpmrhm  33575  issply  33582  esplyval  33583  extdgval  33664  fldextrspundgle  33689  minplyval  33716  constrcon  33785  2sqr3minply  33791  lmatfval  33825  lmat22e11  33829  rrhval  34007  xrhval  34029  brae  34252  braew  34253  sitmval  34360  sseqval  34399  fibp1  34412  elprob  34420  signsvtn0  34581  signstfvneq0  34583  signstfveq0  34588  breprexplema  34641  breprexp  34644  circlevma  34653  circlemethhgt  34654  cvmliftlem5  35331  cvmliftlem7  35333  cvmliftlem10  35336  cvmliftlem13  35338  satefv  35456  mclsval  35605  rdgprc0  35833  dfrdg2  35835  bj-finsumval0  37325  rdgeqoa  37410  finxpeq2  37427  finxpreclem6  37436  finxpsuclem  37437  sdclem2  37788  ldualvsub  39200  ldualvsubval  39202  isopos  39225  polfvalN  39949  psubclsetN  39981  docaffvalN  41166  docafvalN  41167  djaffvalN  41178  djafvalN  41179  dihffval  41275  dihfval  41276  dochffval  41394  dochfval  41395  djhffval  41441  djhfval  41442  islpolN  41528  lcdfval  41633  lcdval  41634  lcdvsub  41662  lcdvsubval  41663  mapdffval  41671  mapdfval  41672  hdmap1fval  41841  hdmapfval  41872  hgmapfval  41931  hdmapglem7  41974  hlhilset  41979  aks6d1c1p1  42146  evlselv  42626  0prjspnrel  42666  ismrc  42740  rmxfval  42943  rmyfval  42944  aomclem8  43100  hbt  43169  elmnc  43175  mncn0  43178  aaitgo  43201  clsk1independent  44085  binomcxp  44396  limciccioolb  45667  limcicciooub  45681  ioccncflimc  45929  icocncflimc  45933  dvnprodlem2  45991  dvnprodlem3  45992  dirkercncflem3  46149  fourierdlem32  46183  etransclem32  46310  etransclem44  46322  etransclem46  46324  etransc  46327  ovnsubaddlem1  46614  ovnsubaddlem2  46615  ovnsubadd  46616  hoidmvlelem4  46642  hoidmvlelem5  46643  hspmbl  46673  vonioo  46726  vonicc  46729  afveq12d  47170  iccelpart  47470  nnsum3primesprm  47827  funcringcsetcALTV2lem7  48333  funcringcsetcALTV2lem9  48335  funcringcsetclem7ALTV  48356  funcringcsetclem9ALTV  48358  cofu1a  49132  cofu2a  49133  cofid1  49152  cofid2  49153  uptr2  49259  swapfida  49318  cofuswapf2  49333  fuco21  49374  fuco23  49379  fucoid  49386  opf2  49444  oppfdiag1  49452  oppfdiag  49454  termolmd  49708