Theorem fveq12d 6841

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

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

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 2115  ax-9 2123  ax-ext 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500

This theorem is referenced by:  nffvd  6846  fvmpopr2d  7520  tfrlem3a  8308  resixpfo  8874  cantnfval  9577  cantnfres  9586  fseqenlem1  9934  fseqenlem2  9935  dfac12lem1  10054  dfac12lem2  10055  dfac12r  10057  hsmexlem2  10337  ttukeylem3  10421  ttukey2g  10426  seq1  13937  expval  13986  lsw  14487  ccatfval  14496  swrdval  14567  splfv2a  14679  revval  14683  relexpsucnnr  14948  relexp1g  14949  seqshft  15008  climshft2  15505  fprodser  15872  imasval  17432  funcid  17794  funcco  17795  funcoppc  17799  funcres  17820  nati  17882  funcestrcsetclem7  18069  funcestrcsetclem9  18071  funcsetcestrclem7  18084  funcsetcestrclem9  18086  evlf2  18141  evlf1  18143  evlfcl  18145  uncf2  18160  hofcl  18182  yonedalem21  18196  yonedalem3a  18197  yonedalem4a  18198  yonedalem4b  18199  yonedalem22  18201  yonedalem3  18203  yonedainv  18204  p0val  18348  p1val  18349  gsumvalx  18601  gsumpropd  18603  gsumval2a  18610  gsumsgrpccat  18765  prdsinvlem  18979  mulgfval  18999  mulgfvalALT  19000  mulgval  19001  mulgnndir  19033  mulgpropd  19046  cntrval  19248  efgsf  19658  efgsval  19660  issrngd  20788  rlmval  21143  chrval  21478  znval  21490  isphl  21583  isphld  21609  phlpropd  21610  cssval  21637  prdsinvgd2  21697  islindf  21767  evlseu  22038  evlval  22055  selvffval  22076  selvval  22078  evls1fval  22263  evl1varpw  22305  madetsumid  22405  madufval  22581  smadiadetr  22619  decpmatval0  22708  chpmatfval  22774  isperf  23095  dfac14  23562  xkohmeo  23759  flffval  23933  fcfval  23977  cnextfval  24006  tsmsval2  24074  tsmspropd  24076  tngngp  24598  tngngp3  24600  isnlm  24619  sranlm  24628  cnncvsabsnegdemo  25121  ovoliunlem1  25459  ovoliunlem2  25460  limcfval  25829  dvfval  25854  dvreslem  25866  dvaddbr  25896  dvmulbr  25897  dvmulbrOLD  25898  isuc1p  26102  ismon1p  26104  mon1pid  26115  q1pval  26116  dgreq0  26227  vieta1lem2  26275  vieta1  26276  basellem5  27051  lgsval  27268  lgsneg  27288  seqseq123d  28282  israg  28769  iswlkon  29729  wlkres  29742  wlkp1lem3  29747  wlkp1lem6  29750  isclwlk  29846  iscrct  29863  iscycl  29864  eupth2eucrct  30292  dipfval  30777  prodindf  32944  splfv3  33040  cycpmco2lem5  33212  cycpmco2lem6  33213  idlsrgval  33584  m1pmeq  33666  mplvrpmfgalem  33709  mplvrpmga  33710  mplvrpmmhm  33711  mplvrpmrhm  33712  issply  33719  esplyval  33720  esplyind  33731  vieta  33736  extdgval  33810  fldextrspundgle  33835  minplyval  33862  constrcon  33931  2sqr3minply  33937  lmatfval  33971  lmat22e11  33975  rrhval  34153  xrhval  34175  brae  34398  braew  34399  sitmval  34506  sseqval  34545  fibp1  34558  elprob  34566  signsvtn0  34727  signstfvneq0  34729  signstfveq0  34734  breprexplema  34787  breprexp  34790  circlevma  34799  circlemethhgt  34800  cvmliftlem5  35483  cvmliftlem7  35485  cvmliftlem10  35488  cvmliftlem13  35490  satefv  35608  mclsval  35757  rdgprc0  35985  dfrdg2  35987  bj-finsumval0  37490  rdgeqoa  37575  finxpeq2  37592  finxpreclem6  37601  finxpsuclem  37602  sdclem2  37943  ldualvsub  39415  ldualvsubval  39417  isopos  39440  polfvalN  40164  psubclsetN  40196  docaffvalN  41381  docafvalN  41382  djaffvalN  41393  djafvalN  41394  dihffval  41490  dihfval  41491  dochffval  41609  dochfval  41610  djhffval  41656  djhfval  41657  islpolN  41743  lcdfval  41848  lcdval  41849  lcdvsub  41877  lcdvsubval  41878  mapdffval  41886  mapdfval  41887  hdmap1fval  42056  hdmapfval  42087  hgmapfval  42146  hdmapglem7  42189  hlhilset  42194  aks6d1c1p1  42361  evlselv  42830  0prjspnrel  42870  ismrc  42943  rmxfval  43146  rmyfval  43147  aomclem8  43303  hbt  43372  elmnc  43378  mncn0  43381  aaitgo  43404  clsk1independent  44287  binomcxp  44598  limciccioolb  45867  limcicciooub  45881  ioccncflimc  46129  icocncflimc  46133  dvnprodlem2  46191  dvnprodlem3  46192  dirkercncflem3  46349  fourierdlem32  46383  etransclem32  46510  etransclem44  46522  etransclem46  46524  etransc  46527  ovnsubaddlem1  46814  ovnsubaddlem2  46815  ovnsubadd  46816  hoidmvlelem4  46842  hoidmvlelem5  46843  hspmbl  46873  vonioo  46926  vonicc  46929  afveq12d  47379  iccelpart  47679  nnsum3primesprm  48036  funcringcsetcALTV2lem7  48542  funcringcsetcALTV2lem9  48544  funcringcsetclem7ALTV  48565  funcringcsetclem9ALTV  48567  cofu1a  49339  cofu2a  49340  cofid1  49359  cofid2  49360  uptr2  49466  swapfida  49525  cofuswapf2  49540  fuco21  49581  fuco23  49586  fucoid  49593  opf2  49651  oppfdiag1  49659  oppfdiag  49661  termolmd  49915