Theorem fveq12d 6833

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494

This theorem is referenced by:  nffvd  6838  fvmpopr2d  7515  tfrlem3a  8306  resixpfo  8870  cantnfval  9583  cantnfres  9592  fseqenlem1  9937  fseqenlem2  9938  dfac12lem1  10057  dfac12lem2  10058  dfac12r  10060  hsmexlem2  10340  ttukeylem3  10424  ttukey2g  10429  seq1  13939  expval  13988  lsw  14489  ccatfval  14498  swrdval  14568  splfv2a  14680  revval  14684  relexpsucnnr  14950  relexp1g  14951  seqshft  15010  climshft2  15507  fprodser  15874  imasval  17433  funcid  17795  funcco  17796  funcoppc  17800  funcres  17821  nati  17883  funcestrcsetclem7  18070  funcestrcsetclem9  18072  funcsetcestrclem7  18085  funcsetcestrclem9  18087  evlf2  18142  evlf1  18144  evlfcl  18146  uncf2  18161  hofcl  18183  yonedalem21  18197  yonedalem3a  18198  yonedalem4a  18199  yonedalem4b  18200  yonedalem22  18202  yonedalem3  18204  yonedainv  18205  p0val  18349  p1val  18350  gsumvalx  18568  gsumpropd  18570  gsumval2a  18577  gsumsgrpccat  18732  prdsinvlem  18946  mulgfval  18966  mulgfvalALT  18967  mulgval  18968  mulgnndir  19000  mulgpropd  19013  cntrval  19216  efgsf  19626  efgsval  19628  issrngd  20758  rlmval  21113  chrval  21448  znval  21460  isphl  21553  isphld  21579  phlpropd  21580  cssval  21607  prdsinvgd2  21667  islindf  21737  evlseu  22006  evlval  22018  selvffval  22036  selvval  22038  evls1fval  22222  evl1varpw  22264  madetsumid  22364  madufval  22540  smadiadetr  22578  decpmatval0  22667  chpmatfval  22733  isperf  23054  dfac14  23521  xkohmeo  23718  flffval  23892  fcfval  23936  cnextfval  23965  tsmsval2  24033  tsmspropd  24035  tngngp  24558  tngngp3  24560  isnlm  24579  sranlm  24588  cnncvsabsnegdemo  25081  ovoliunlem1  25419  ovoliunlem2  25420  limcfval  25789  dvfval  25814  dvreslem  25826  dvaddbr  25856  dvmulbr  25857  dvmulbrOLD  25858  isuc1p  26062  ismon1p  26064  mon1pid  26075  q1pval  26076  dgreq0  26187  vieta1lem2  26235  vieta1  26236  basellem5  27011  lgsval  27228  lgsneg  27248  seqseq123d  28203  israg  28660  iswlkon  29619  wlkres  29632  wlkp1lem3  29637  wlkp1lem6  29640  isclwlk  29736  iscrct  29753  iscycl  29754  eupth2eucrct  30179  dipfval  30664  prodindf  32819  splfv3  32913  cycpmco2lem5  33085  cycpmco2lem6  33086  idlsrgval  33453  m1pmeq  33531  extdgval  33628  fldextrspundgle  33652  minplyval  33674  constrcon  33743  2sqr3minply  33749  lmatfval  33783  lmat22e11  33787  rrhval  33965  xrhval  33987  brae  34210  braew  34211  sitmval  34319  sseqval  34358  fibp1  34371  elprob  34379  signsvtn0  34540  signstfvneq0  34542  signstfveq0  34547  breprexplema  34600  breprexp  34603  circlevma  34612  circlemethhgt  34613  cvmliftlem5  35264  cvmliftlem7  35266  cvmliftlem10  35269  cvmliftlem13  35271  satefv  35389  mclsval  35538  rdgprc0  35769  dfrdg2  35771  bj-finsumval0  37261  rdgeqoa  37346  finxpeq2  37363  finxpreclem6  37372  finxpsuclem  37373  sdclem2  37724  ldualvsub  39136  ldualvsubval  39138  isopos  39161  polfvalN  39886  psubclsetN  39918  docaffvalN  41103  docafvalN  41104  djaffvalN  41115  djafvalN  41116  dihffval  41212  dihfval  41213  dochffval  41331  dochfval  41332  djhffval  41378  djhfval  41379  islpolN  41465  lcdfval  41570  lcdval  41571  lcdvsub  41599  lcdvsubval  41600  mapdffval  41608  mapdfval  41609  hdmap1fval  41778  hdmapfval  41809  hgmapfval  41868  hdmapglem7  41911  hlhilset  41916  aks6d1c1p1  42083  evlselv  42563  0prjspnrel  42603  ismrc  42677  rmxfval  42880  rmyfval  42881  aomclem8  43037  hbt  43106  elmnc  43112  mncn0  43115  aaitgo  43138  clsk1independent  44022  binomcxp  44333  limciccioolb  45606  limcicciooub  45622  ioccncflimc  45870  icocncflimc  45874  dvnprodlem2  45932  dvnprodlem3  45933  dirkercncflem3  46090  fourierdlem32  46124  etransclem32  46251  etransclem44  46263  etransclem46  46265  etransc  46268  ovnsubaddlem1  46555  ovnsubaddlem2  46556  ovnsubadd  46557  hoidmvlelem4  46583  hoidmvlelem5  46584  hspmbl  46614  vonioo  46667  vonicc  46670  afveq12d  47121  iccelpart  47421  nnsum3primesprm  47778  funcringcsetcALTV2lem7  48284  funcringcsetcALTV2lem9  48286  funcringcsetclem7ALTV  48307  funcringcsetclem9ALTV  48309  cofu1a  49083  cofu2a  49084  cofid1  49103  cofid2  49104  uptr2  49210  swapfida  49269  cofuswapf2  49284  fuco21  49325  fuco23  49330  fucoid  49337  opf2  49395  oppfdiag1  49403  oppfdiag  49405  termolmd  49659