Theorem fveq12d 6918

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ‘cfv 6561

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6515  df-fv 6569

This theorem is used by:  nffvd  6923  fvmpopr2d  7609  tfrlem3a  8415  resixpfo  8995  cantnfval  9699  cantnfres  9708  fseqenlem1  10133  fseqenlem2  10134  dfac12lem1  10252  dfac12lem2  10253  dfac12r  10255  hsmexlem2  10535  ttukeylem3  10619  ttukey2g  10624  seq1  14187  expval  14236  lsw  14739  ccatfval  14748  swrdval  14822  splfv2a  14936  revval  14940  relexpsucnnr  15210  relexp1g  15211  seqshft  15270  climshft2  15781  fprodser  16148  imasval  17715  funcid  18077  funcco  18078  funcoppc  18082  funcres  18103  nati  18165  funcestrcsetclem7  18352  funcestrcsetclem9  18354  funcsetcestrclem7  18367  funcsetcestrclem9  18369  evlf2  18424  evlf1  18426  evlfcl  18428  uncf2  18443  hofcl  18465  yonedalem21  18479  yonedalem3a  18480  yonedalem4a  18481  yonedalem4b  18482  yonedalem22  18484  yonedalem3  18486  yonedainv  18487  p0val  18631  p1val  18632  gsumvalx  18897  gsumpropd  18899  gsumval2a  18906  gsumsgrpccat  19068  prdsinvlem  19291  mulgfval  19311  mulgfvalALT  19312  mulgval  19313  mulgnndir  19345  mulgpropd  19358  cntrval  19566  efgsf  19976  efgsval  19978  issrngd  21145  rlmval  21499  chrval  21862  znval  21874  isphl  21967  isphld  21993  phlpropd  21994  cssval  22021  prdsinvgd2  22081  islindf  22151  evlseu  22425  evlval  22442  selvffval  22460  selvval  22462  evls1fval  22670  evl1varpw  22712  madetsumid  22809  madufval  22985  smadiadetr  23023  decpmatval0  23115  chpmatfval  23181  isperf  23502  dfac14  23970  xkohmeo  24167  flffval  24341  fcfval  24385  cnextfval  24414  tsmsval2  24482  tsmspropd  24484  tngngp  25006  tngngp3  25008  isnlm  25027  sranlm  25036  cnncvsabsnegdemo  25519  ovoliunlem1  25856  ovoliunlem2  25857  limcfval  26225  dvfval  26250  dvreslem  26262  dvaddbr  26291  dvmulbr  26292  isuc1p  26492  ismon1p  26494  mon1pid  26505  q1pval  26506  dgreq0  26617  vieta1lem2  26667  vieta1  26668  basellem5  27445  lgsval  27661  lgsneg  27681  seqseq123d  28705  israg  29205  angmgmaddeu1  29412  iswlkon  30269  wlkres  30282  wlkp1lem3  30287  wlkp1lem6  30290  isclwlk  30393  iscrct  30410  iscycl  30411  eupth2eucrct  30851  dipfval  31337  prodindf  33502  splfv3  33592  cycpmco2lem5  33767  cycpmco2lem6  33768  idlsrgval  34119  m1pmeq  34200  mplvrpmfgalem  34259  mplvrpmga  34260  mplvrpmmhm  34261  mplvrpmrhm  34262  issply  34276  esplyval  34277  esplyind  34290  vieta  34295  extdgval  34368  fldextrspundgle  34393  minplyval  34420  constrcon  34489  2sqr3minply  34495  lmatfval  34529  lmat22e11  34533  rrhval  34711  xrhval  34733  brae  34957  braew  34958  sitmval  35064  sseqval  35103  fibp1  35116  elprob  35124  signsvtn0  35282  signstfvneq0  35284  signstfveq0  35289  breprexplema  35342  breprexp  35345  circlevma  35354  circlemethhgt  35355  fnlfvk3n0  36041  onf1oracwevd  36065  cvmliftlem5  36234  cvmliftlem7  36236  cvmliftlem10  36239  cvmliftlem13  36241  satefv  36359  mclsval  36508  rdgprc0  36746  dfrdg2  36748  bj-finsumval0  38411  rdgeqoa  38498  finxpeq2  38515  finxpreclem6  38524  finxpsuclem  38525  sdclem2  38879  ldualvsub  40415  ldualvsubval  40417  isopos  40440  polfvalN  41164  psubclsetN  41196  docaffvalN  42381  docafvalN  42382  djaffvalN  42393  djafvalN  42394  dihffval  42490  dihfval  42491  dochffval  42609  dochfval  42610  djhffval  42656  djhfval  42657  islpolN  42743  lcdfval  42848  lcdval  42849  lcdvsub  42877  lcdvsubval  42878  mapdffval  42886  mapdfval  42887  hdmap1fval  43056  hdmapfval  43087  hgmapfval  43146  hdmapglem7  43189  hlhilset  43194  aks6d1c1p1  43360  evlselv  43821  prjspnnormval  43863  0prjspnrel  43867  ismrc  43916  rmxfval  44115  rmyfval  44116  aomclem8  44267  hbt  44335  elmnc  44341  mncn0  44344  aaitgo  44367  clsk1independent  45249  binomcxp  45544  limciccioolb  46848  limcicciooub  46862  ioccncflimc  47110  icocncflimc  47114  dvnprodlem2  47172  dvnprodlem3  47173  dirkercncflem3  47330  fourierdlem32  47364  etransclem32  47491  etransclem44  47503  etransclem46  47505  etransc  47508  ovnsubaddlem1  47795  ovnsubaddlem2  47796  ovnsubadd  47797  hoidmvlelem4  47823  hoidmvlelem5  47824  hspmbl  47854  vonioo  47907  vonicc  47910  afveq12d  48418  iccelpart  48730  nnsum3primesprm  49103  funcringcsetcALTV2lem7  49608  funcringcsetcALTV2lem9  49610  funcringcsetclem7ALTV  49631  funcringcsetclem9ALTV  49633  cofu1a  50424  cofu2a  50425  cofid1  50445  cofid2  50446  uptr2  50552  swapfida  50617  cofuswapf2  50632  fuco21  50673  fuco23  50678  fucoid  50685  fucoaltvallem  50707  postcof2  50715  opf2  50756  oppfdiag1  50764  oppfdiag  50766  termolmd  51068