Theorem fveq12d 6835

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

Syntax hints:   → wi 4   = wceq 1547  ‘cfv 6486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4263  df-if 4456  df-sn 4557  df-pr 4559  df-op 4563  df-uni 4840  df-br 5074  df-iota 6442  df-fv 6494

This theorem is referenced by:  nffvd  6840  fvmpopr2d  7519  tfrlem3a  8307  resixpfo  8875  cantnfval  9581  cantnfres  9590  fseqenlem1  9938  fseqenlem2  9939  dfac12lem1  10058  dfac12lem2  10059  dfac12r  10061  hsmexlem2  10341  ttukeylem3  10425  ttukey2g  10430  seq1  13968  expval  14017  lsw  14518  ccatfval  14527  swrdval  14598  splfv2a  14710  revval  14714  relexpsucnnr  14979  relexp1g  14980  seqshft  15039  climshft2  15536  fprodser  15906  imasval  17467  funcid  17829  funcco  17830  funcoppc  17834  funcres  17855  nati  17917  funcestrcsetclem7  18104  funcestrcsetclem9  18106  funcsetcestrclem7  18119  funcsetcestrclem9  18121  evlf2  18176  evlf1  18178  evlfcl  18180  uncf2  18195  hofcl  18217  yonedalem21  18231  yonedalem3a  18232  yonedalem4a  18233  yonedalem4b  18234  yonedalem22  18236  yonedalem3  18238  yonedainv  18239  p0val  18383  p1val  18384  gsumvalx  18636  gsumpropd  18638  gsumval2a  18645  gsumsgrpccat  18800  prdsinvlem  19017  mulgfval  19037  mulgfvalALT  19038  mulgval  19039  mulgnndir  19071  mulgpropd  19084  cntrval  19286  efgsf  19696  efgsval  19698  issrngd  20828  rlmval  21182  chrval  21499  znval  21511  isphl  21604  isphld  21630  phlpropd  21631  cssval  21658  prdsinvgd2  21718  islindf  21788  evlseu  22060  evlval  22077  selvffval  22095  selvval  22097  evls1fval  22306  evl1varpw  22348  madetsumid  22445  madufval  22621  smadiadetr  22659  decpmatval0  22748  chpmatfval  22814  isperf  23135  dfac14  23602  xkohmeo  23799  flffval  23973  fcfval  24017  cnextfval  24046  tsmsval2  24114  tsmspropd  24116  tngngp  24638  tngngp3  24640  isnlm  24659  sranlm  24668  cnncvsabsnegdemo  25151  ovoliunlem1  25488  ovoliunlem2  25489  limcfval  25858  dvfval  25883  dvreslem  25895  dvaddbr  25924  dvmulbr  25925  isuc1p  26125  ismon1p  26127  mon1pid  26138  q1pval  26139  dgreq0  26249  vieta1lem2  26296  vieta1  26297  basellem5  27067  lgsval  27283  lgsneg  27303  seqseq123d  28297  israg  28784  iswlkon  29743  wlkres  29756  wlkp1lem3  29761  wlkp1lem6  29764  isclwlk  29860  iscrct  29877  iscycl  29878  eupth2eucrct  30306  dipfval  30792  prodindf  32942  splfv3  33038  cycpmco2lem5  33212  cycpmco2lem6  33213  idlsrgval  33595  m1pmeq  33677  mplvrpmfgalem  33737  mplvrpmga  33738  mplvrpmmhm  33739  mplvrpmrhm  33740  issply  33754  esplyval  33755  esplyind  33768  vieta  33773  extdgval  33846  fldextrspundgle  33871  minplyval  33898  constrcon  33967  2sqr3minply  33973  lmatfval  34007  lmat22e11  34011  rrhval  34189  xrhval  34211  brae  34434  braew  34435  sitmval  34542  sseqval  34581  fibp1  34594  elprob  34602  signsvtn0  34763  signstfvneq0  34765  signstfveq0  34770  breprexplema  34823  breprexp  34826  circlevma  34835  circlemethhgt  34836  cvmliftlem5  35526  cvmliftlem7  35528  cvmliftlem10  35531  cvmliftlem13  35533  satefv  35651  mclsval  35800  rdgprc0  36028  dfrdg2  36030  bj-finsumval0  37654  rdgeqoa  37741  finxpeq2  37758  finxpreclem6  37767  finxpsuclem  37768  sdclem2  38118  ldualvsub  39656  ldualvsubval  39658  isopos  39681  polfvalN  40405  psubclsetN  40437  docaffvalN  41622  docafvalN  41623  djaffvalN  41634  djafvalN  41635  dihffval  41731  dihfval  41732  dochffval  41850  dochfval  41851  djhffval  41897  djhfval  41898  islpolN  41984  lcdfval  42089  lcdval  42090  lcdvsub  42118  lcdvsubval  42119  mapdffval  42127  mapdfval  42128  hdmap1fval  42297  hdmapfval  42328  hgmapfval  42387  hdmapglem7  42430  hlhilset  42435  aks6d1c1p1  42601  evlselv  43048  0prjspnrel  43086  ismrc  43159  rmxfval  43358  rmyfval  43359  aomclem8  43515  hbt  43584  elmnc  43590  mncn0  43593  aaitgo  43616  clsk1independent  44499  binomcxp  44810  limciccioolb  46074  limcicciooub  46088  ioccncflimc  46336  icocncflimc  46340  dvnprodlem2  46398  dvnprodlem3  46399  dirkercncflem3  46556  fourierdlem32  46590  etransclem32  46717  etransclem44  46729  etransclem46  46731  etransc  46734  ovnsubaddlem1  47021  ovnsubaddlem2  47022  ovnsubadd  47023  hoidmvlelem4  47049  hoidmvlelem5  47050  hspmbl  47080  vonioo  47133  vonicc  47136  afveq12d  47604  iccelpart  47916  nnsum3primesprm  48289  funcringcsetcALTV2lem7  48795  funcringcsetcALTV2lem9  48797  funcringcsetclem7ALTV  48818  funcringcsetclem9ALTV  48820  cofu1a  49592  cofu2a  49593  cofid1  49612  cofid2  49613  uptr2  49719  swapfida  49778  cofuswapf2  49793  fuco21  49834  fuco23  49839  fucoid  49846  opf2  49904  oppfdiag1  49912  oppfdiag  49914  termolmd  50168