Theorem fveq12d 6880

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

Syntax hints:   → wi 4   = wceq 1539  ‘cfv 6528

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3414  df-v 3459  df-dif 3927  df-un 3929  df-ss 3941  df-nul 4307  df-if 4499  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4882  df-br 5118  df-iota 6481  df-fv 6536

This theorem is referenced by:  nffvd  6885  fvmpopr2d  7564  wrecseq123OLD  8309  tfrlem3a  8386  resixpfo  8945  cantnfval  9675  cantnfres  9684  fseqenlem1  10031  fseqenlem2  10032  dfac12lem1  10151  dfac12lem2  10152  dfac12r  10154  hsmexlem2  10434  ttukeylem3  10518  ttukey2g  10523  seq1  14022  expval  14071  lsw  14571  ccatfval  14580  swrdval  14650  splfv2a  14763  revval  14767  relexpsucnnr  15033  relexp1g  15034  seqshft  15093  climshft2  15587  fprodser  15954  imasval  17512  funcid  17870  funcco  17871  funcoppc  17875  funcres  17896  nati  17958  funcestrcsetclem7  18145  funcestrcsetclem9  18147  funcsetcestrclem7  18160  funcsetcestrclem9  18162  evlf2  18217  evlf1  18219  evlfcl  18221  uncf2  18236  hofcl  18258  yonedalem21  18272  yonedalem3a  18273  yonedalem4a  18274  yonedalem4b  18275  yonedalem22  18277  yonedalem3  18279  yonedainv  18280  p0val  18424  p1val  18425  gsumvalx  18641  gsumpropd  18643  gsumval2a  18650  gsumsgrpccat  18805  prdsinvlem  19019  mulgfval  19039  mulgfvalALT  19040  mulgval  19041  mulgnndir  19073  mulgpropd  19086  cntrval  19289  efgsf  19697  efgsval  19699  issrngd  20802  rlmval  21136  chrval  21471  znval  21483  isphl  21575  isphld  21601  phlpropd  21602  cssval  21629  prdsinvgd2  21689  islindf  21759  evlseu  22028  evlval  22040  selvffval  22058  selvval  22060  evls1fval  22244  evl1varpw  22286  madetsumid  22386  madufval  22562  smadiadetr  22600  decpmatval0  22689  chpmatfval  22755  isperf  23076  dfac14  23543  xkohmeo  23740  flffval  23914  fcfval  23958  cnextfval  23987  tsmsval2  24055  tsmspropd  24057  tngngp  24580  tngngp3  24582  isnlm  24601  sranlm  24610  cnncvsabsnegdemo  25104  ovoliunlem1  25442  ovoliunlem2  25443  limcfval  25812  dvfval  25837  dvreslem  25849  dvaddbr  25879  dvmulbr  25880  dvmulbrOLD  25881  isuc1p  26085  ismon1p  26087  mon1pid  26098  q1pval  26099  dgreq0  26210  vieta1lem2  26258  vieta1  26259  basellem5  27033  lgsval  27250  lgsneg  27270  seqseq123d  28197  israg  28610  iswlkon  29571  wlkres  29584  wlkp1lem3  29589  wlkp1lem6  29592  isclwlk  29689  iscrct  29706  iscycl  29707  eupth2eucrct  30132  dipfval  30617  prodindf  32777  splfv3  32872  cycpmco2lem5  33078  cycpmco2lem6  33079  idlsrgval  33455  m1pmeq  33532  extdgval  33630  fldextrspundgle  33654  minplyval  33674  constrcon  33743  2sqr3minply  33749  lmatfval  33774  lmat22e11  33778  rrhval  33956  xrhval  33978  brae  34201  braew  34202  sitmval  34310  sseqval  34349  fibp1  34362  elprob  34370  signsvtn0  34531  signstfvneq0  34533  signstfveq0  34538  breprexplema  34591  breprexp  34594  circlevma  34603  circlemethhgt  34604  cvmliftlem5  35240  cvmliftlem7  35242  cvmliftlem10  35245  cvmliftlem13  35247  satefv  35365  mclsval  35514  rdgprc0  35740  dfrdg2  35742  bj-finsumval0  37232  rdgeqoa  37317  finxpeq2  37334  finxpreclem6  37343  finxpsuclem  37344  sdclem2  37695  ldualvsub  39102  ldualvsubval  39104  isopos  39127  polfvalN  39852  psubclsetN  39884  docaffvalN  41069  docafvalN  41070  djaffvalN  41081  djafvalN  41082  dihffval  41178  dihfval  41179  dochffval  41297  dochfval  41298  djhffval  41344  djhfval  41345  islpolN  41431  lcdfval  41536  lcdval  41537  lcdvsub  41565  lcdvsubval  41566  mapdffval  41574  mapdfval  41575  hdmap1fval  41744  hdmapfval  41775  hgmapfval  41834  hdmapglem7  41877  hlhilset  41882  aks6d1c1p1  42049  evlselv  42542  0prjspnrel  42582  ismrc  42656  rmxfval  42859  rmyfval  42860  aomclem8  43017  hbt  43086  elmnc  43092  mncn0  43095  aaitgo  43118  clsk1independent  44002  binomcxp  44314  limciccioolb  45586  limcicciooub  45602  ioccncflimc  45850  icocncflimc  45854  dvnprodlem2  45912  dvnprodlem3  45913  dirkercncflem3  46070  fourierdlem32  46104  etransclem32  46231  etransclem44  46243  etransclem46  46245  etransc  46248  ovnsubaddlem1  46535  ovnsubaddlem2  46536  ovnsubadd  46537  hoidmvlelem4  46563  hoidmvlelem5  46564  hspmbl  46594  vonioo  46647  vonicc  46650  afveq12d  47098  iccelpart  47373  nnsum3primesprm  47730  funcringcsetcALTV2lem7  48165  funcringcsetcALTV2lem9  48167  funcringcsetclem7ALTV  48188  funcringcsetclem9ALTV  48190  swapfida  49060  cofuswapf2  49069  fuco21  49110  fuco23  49115  fucoid  49122