Theorem fveq12d 6927

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

Syntax hints:   → wi 4   = wceq 1537  ‘cfv 6573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581

This theorem is referenced by:  nffvd  6932  fvmpopr2d  7612  wrecseq123OLD  8356  tfrlem3a  8433  resixpfo  8994  cantnfval  9737  cantnfres  9746  fseqenlem1  10093  fseqenlem2  10094  dfac12lem1  10213  dfac12lem2  10214  dfac12r  10216  hsmexlem2  10496  ttukeylem3  10580  ttukey2g  10585  seq1  14065  expval  14114  lsw  14612  ccatfval  14621  swrdval  14691  splfv2a  14804  revval  14808  relexpsucnnr  15074  relexp1g  15075  seqshft  15134  climshft2  15628  fprodser  15997  imasval  17571  funcid  17934  funcco  17935  funcoppc  17939  funcres  17960  nati  18023  funcestrcsetclem7  18215  funcestrcsetclem9  18217  funcsetcestrclem7  18230  funcsetcestrclem9  18232  evlf2  18288  evlf1  18290  evlfcl  18292  uncf2  18307  hofcl  18329  yonedalem21  18343  yonedalem3a  18344  yonedalem4a  18345  yonedalem4b  18346  yonedalem22  18348  yonedalem3  18350  yonedainv  18351  p0val  18497  p1val  18498  gsumvalx  18714  gsumpropd  18716  gsumval2a  18723  gsumsgrpccat  18875  prdsinvlem  19089  mulgfval  19109  mulgfvalALT  19110  mulgval  19111  mulgnndir  19143  mulgpropd  19156  cntrval  19359  efgsf  19771  efgsval  19773  issrngd  20878  rlmval  21221  chrval  21561  znval  21573  isphl  21669  isphld  21695  phlpropd  21696  cssval  21723  prdsinvgd2  21785  islindf  21855  evlseu  22130  evlval  22142  selvffval  22160  selvval  22162  evls1fval  22344  evl1varpw  22386  madetsumid  22488  madufval  22664  smadiadetr  22702  decpmatval0  22791  chpmatfval  22857  isperf  23180  dfac14  23647  xkohmeo  23844  flffval  24018  fcfval  24062  cnextfval  24091  tsmsval2  24159  tsmspropd  24161  tngngp  24696  tngngp3  24698  isnlm  24717  sranlm  24726  cnncvsabsnegdemo  25218  ovoliunlem1  25556  ovoliunlem2  25557  limcfval  25927  dvfval  25952  dvreslem  25964  dvaddbr  25994  dvmulbr  25995  dvmulbrOLD  25996  isuc1p  26200  ismon1p  26202  mon1pid  26213  q1pval  26214  dgreq0  26325  vieta1lem2  26371  vieta1  26372  basellem5  27146  lgsval  27363  lgsneg  27383  seqseq123d  28310  israg  28723  iswlkon  29693  wlkres  29706  wlkp1lem3  29711  wlkp1lem6  29714  isclwlk  29809  iscrct  29826  iscycl  29827  eupth2eucrct  30249  dipfval  30734  splfv3  32925  cycpmco2lem5  33123  cycpmco2lem6  33124  idlsrgval  33496  m1pmeq  33573  extdgval  33667  minplyval  33698  2sqr3minply  33738  lmatfval  33760  lmat22e11  33764  rrhval  33942  xrhval  33964  prodindf  33987  brae  34205  braew  34206  sitmval  34314  sseqval  34353  fibp1  34366  elprob  34374  signsvtn0  34547  signstfvneq0  34549  signstfveq0  34554  breprexplema  34607  breprexp  34610  circlevma  34619  circlemethhgt  34620  cvmliftlem5  35257  cvmliftlem7  35259  cvmliftlem10  35262  cvmliftlem13  35264  satefv  35382  mclsval  35531  rdgprc0  35757  dfrdg2  35759  bj-finsumval0  37251  rdgeqoa  37336  finxpeq2  37353  finxpreclem6  37362  finxpsuclem  37363  sdclem2  37702  ldualvsub  39111  ldualvsubval  39113  isopos  39136  polfvalN  39861  psubclsetN  39893  docaffvalN  41078  docafvalN  41079  djaffvalN  41090  djafvalN  41091  dihffval  41187  dihfval  41188  dochffval  41306  dochfval  41307  djhffval  41353  djhfval  41354  islpolN  41440  lcdfval  41545  lcdval  41546  lcdvsub  41574  lcdvsubval  41575  mapdffval  41583  mapdfval  41584  hdmap1fval  41753  hdmapfval  41784  hgmapfval  41843  hdmapglem7  41886  hlhilset  41891  aks6d1c1p1  42064  evlselv  42542  0prjspnrel  42582  ismrc  42657  rmxfval  42860  rmyfval  42861  aomclem8  43018  hbt  43087  elmnc  43093  mncn0  43096  aaitgo  43119  clsk1independent  44008  binomcxp  44326  limciccioolb  45542  limcicciooub  45558  ioccncflimc  45806  icocncflimc  45810  dvnprodlem2  45868  dvnprodlem3  45869  dirkercncflem3  46026  fourierdlem32  46060  etransclem32  46187  etransclem44  46199  etransclem46  46201  etransc  46204  ovnsubaddlem1  46491  ovnsubaddlem2  46492  ovnsubadd  46493  hoidmvlelem4  46519  hoidmvlelem5  46520  hspmbl  46550  vonioo  46603  vonicc  46606  afveq12d  47048  iccelpart  47307  nnsum3primesprm  47664  funcringcsetcALTV2lem7  48019  funcringcsetcALTV2lem9  48021  funcringcsetclem7ALTV  48042  funcringcsetclem9ALTV  48044