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 2775	1 ⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐵))

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

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 2712

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 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500

This theorem is referenced by:  nffvd  6846  fvmpopr2d  7525  tfrlem3a  8313  resixpfo  8881  cantnfval  9587  cantnfres  9596  fseqenlem1  9944  fseqenlem2  9945  dfac12lem1  10064  dfac12lem2  10065  dfac12r  10067  hsmexlem2  10347  ttukeylem3  10431  ttukey2g  10436  seq1  13974  expval  14023  lsw  14524  ccatfval  14533  swrdval  14604  splfv2a  14716  revval  14720  relexpsucnnr  14985  relexp1g  14986  seqshft  15045  climshft2  15542  fprodser  15912  imasval  17473  funcid  17835  funcco  17836  funcoppc  17840  funcres  17861  nati  17923  funcestrcsetclem7  18110  funcestrcsetclem9  18112  funcsetcestrclem7  18125  funcsetcestrclem9  18127  evlf2  18182  evlf1  18184  evlfcl  18186  uncf2  18201  hofcl  18223  yonedalem21  18237  yonedalem3a  18238  yonedalem4a  18239  yonedalem4b  18240  yonedalem22  18242  yonedalem3  18244  yonedainv  18245  p0val  18389  p1val  18390  gsumvalx  18642  gsumpropd  18644  gsumval2a  18651  gsumsgrpccat  18806  prdsinvlem  19023  mulgfval  19043  mulgfvalALT  19044  mulgval  19045  mulgnndir  19077  mulgpropd  19090  cntrval  19292  efgsf  19702  efgsval  19704  issrngd  20834  rlmval  21188  chrval  21505  znval  21517  isphl  21610  isphld  21636  phlpropd  21637  cssval  21664  prdsinvgd2  21724  islindf  21794  evlseu  22066  evlval  22083  selvffval  22101  selvval  22103  evls1fval  22312  evl1varpw  22354  madetsumid  22451  madufval  22627  smadiadetr  22665  decpmatval0  22754  chpmatfval  22820  isperf  23141  dfac14  23608  xkohmeo  23805  flffval  23979  fcfval  24023  cnextfval  24052  tsmsval2  24120  tsmspropd  24122  tngngp  24644  tngngp3  24646  isnlm  24665  sranlm  24674  cnncvsabsnegdemo  25157  ovoliunlem1  25494  ovoliunlem2  25495  limcfval  25864  dvfval  25889  dvreslem  25901  dvaddbr  25930  dvmulbr  25931  isuc1p  26131  ismon1p  26133  mon1pid  26144  q1pval  26145  dgreq0  26255  vieta1lem2  26302  vieta1  26303  basellem5  27073  lgsval  27289  lgsneg  27309  seqseq123d  28303  israg  28790  iswlkon  29749  wlkres  29762  wlkp1lem3  29767  wlkp1lem6  29770  isclwlk  29866  iscrct  29883  iscycl  29884  eupth2eucrct  30312  dipfval  30798  prodindf  32948  splfv3  33044  cycpmco2lem5  33218  cycpmco2lem6  33219  idlsrgval  33593  m1pmeq  33675  mplvrpmfgalem  33735  mplvrpmga  33736  mplvrpmmhm  33737  mplvrpmrhm  33738  issply  33752  esplyval  33753  esplyind  33766  vieta  33771  extdgval  33844  fldextrspundgle  33869  minplyval  33896  constrcon  33965  2sqr3minply  33971  lmatfval  34005  lmat22e11  34009  rrhval  34187  xrhval  34209  brae  34432  braew  34433  sitmval  34540  sseqval  34579  fibp1  34592  elprob  34600  signsvtn0  34761  signstfvneq0  34763  signstfveq0  34768  breprexplema  34821  breprexp  34824  circlevma  34833  circlemethhgt  34834  cvmliftlem5  35524  cvmliftlem7  35526  cvmliftlem10  35529  cvmliftlem13  35531  satefv  35649  mclsval  35798  rdgprc0  36026  dfrdg2  36028  bj-finsumval0  37652  rdgeqoa  37739  finxpeq2  37756  finxpreclem6  37765  finxpsuclem  37766  sdclem2  38116  ldualvsub  39654  ldualvsubval  39656  isopos  39679  polfvalN  40403  psubclsetN  40435  docaffvalN  41620  docafvalN  41621  djaffvalN  41632  djafvalN  41633  dihffval  41729  dihfval  41730  dochffval  41848  dochfval  41849  djhffval  41895  djhfval  41896  islpolN  41982  lcdfval  42087  lcdval  42088  lcdvsub  42116  lcdvsubval  42117  mapdffval  42125  mapdfval  42126  hdmap1fval  42295  hdmapfval  42326  hgmapfval  42385  hdmapglem7  42428  hlhilset  42433  aks6d1c1p1  42599  evlselv  43046  0prjspnrel  43084  ismrc  43157  rmxfval  43356  rmyfval  43357  aomclem8  43513  hbt  43582  elmnc  43588  mncn0  43591  aaitgo  43614  clsk1independent  44497  binomcxp  44808  limciccioolb  46073  limcicciooub  46087  ioccncflimc  46335  icocncflimc  46339  dvnprodlem2  46397  dvnprodlem3  46398  dirkercncflem3  46555  fourierdlem32  46589  etransclem32  46716  etransclem44  46728  etransclem46  46730  etransc  46733  ovnsubaddlem1  47020  ovnsubaddlem2  47021  ovnsubadd  47022  hoidmvlelem4  47048  hoidmvlelem5  47049  hspmbl  47079  vonioo  47132  vonicc  47135  afveq12d  47603  iccelpart  47915  nnsum3primesprm  48288  funcringcsetcALTV2lem7  48794  funcringcsetcALTV2lem9  48796  funcringcsetclem7ALTV  48817  funcringcsetclem9ALTV  48819  cofu1a  49591  cofu2a  49592  cofid1  49611  cofid2  49612  uptr2  49718  swapfida  49777  cofuswapf2  49792  fuco21  49833  fuco23  49838  fucoid  49845  opf2  49903  oppfdiag1  49911  oppfdiag  49913  termolmd  50167