Theorem fveq12d 6893

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  ‘cfv 6539

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6547

This theorem is used by:  nffvd  6898  fvmpopr2d  7583  tfrlem3a  8388  resixpfo  8968  cantnfval  9673  cantnfres  9682  fseqenlem1  10107  fseqenlem2  10108  dfac12lem1  10226  dfac12lem2  10227  dfac12r  10229  hsmexlem2  10509  ttukeylem3  10593  ttukey2g  10598  seq1  14161  expval  14210  lsw  14713  ccatfval  14722  swrdval  14796  splfv2a  14910  revval  14914  relexpsucnnr  15184  relexp1g  15185  seqshft  15244  climshft2  15755  fprodser  16122  imasval  17689  funcid  18051  funcco  18052  funcoppc  18056  funcres  18077  nati  18139  funcestrcsetclem7  18326  funcestrcsetclem9  18328  funcsetcestrclem7  18341  funcsetcestrclem9  18343  evlf2  18398  evlf1  18400  evlfcl  18402  uncf2  18417  hofcl  18439  yonedalem21  18453  yonedalem3a  18454  yonedalem4a  18455  yonedalem4b  18456  yonedalem22  18458  yonedalem3  18460  yonedainv  18461  p0val  18605  p1val  18606  gsumvalx  18871  gsumpropd  18873  gsumval2a  18880  gsumsgrpccat  19042  prdsinvlem  19265  mulgfval  19285  mulgfvalALT  19286  mulgval  19287  mulgnndir  19319  mulgpropd  19332  cntrval  19539  efgsf  19949  efgsval  19951  issrngd  21118  rlmval  21472  chrval  21835  znval  21847  isphl  21940  isphld  21966  phlpropd  21967  cssval  21994  prdsinvgd2  22054  islindf  22124  evlseu  22398  evlval  22415  selvffval  22433  selvval  22435  evls1fval  22643  evl1varpw  22685  madetsumid  22782  madufval  22958  smadiadetr  22996  decpmatval0  23088  chpmatfval  23154  isperf  23475  dfac14  23943  xkohmeo  24140  flffval  24314  fcfval  24358  cnextfval  24387  tsmsval2  24455  tsmspropd  24457  tngngp  24979  tngngp3  24981  isnlm  25000  sranlm  25009  cnncvsabsnegdemo  25492  ovoliunlem1  25829  ovoliunlem2  25830  limcfval  26198  dvfval  26223  dvreslem  26235  dvaddbr  26264  dvmulbr  26265  isuc1p  26465  ismon1p  26467  mon1pid  26478  q1pval  26479  dgreq0  26590  vieta1lem2  26640  vieta1  26641  basellem5  27418  lgsval  27634  lgsneg  27654  seqseq123d  28678  israg  29178  angmgmaddeu1  29385  iswlkon  30242  wlkres  30255  wlkp1lem3  30260  wlkp1lem6  30263  isclwlk  30366  iscrct  30383  iscycl  30384  eupth2eucrct  30824  dipfval  31310  prodindf  33476  splfv3  33566  cycpmco2lem5  33738  cycpmco2lem6  33739  idlsrgval  34082  m1pmeq  34164  mplvrpmfgalem  34223  mplvrpmga  34224  mplvrpmmhm  34225  mplvrpmrhm  34226  issply  34240  esplyval  34241  esplyind  34254  vieta  34259  extdgval  34332  fldextrspundgle  34357  minplyval  34384  constrcon  34453  2sqr3minply  34459  lmatfval  34493  lmat22e11  34497  rrhval  34675  xrhval  34697  brae  34921  braew  34922  sitmval  35028  sseqval  35067  fibp1  35080  elprob  35088  signsvtn0  35246  signstfvneq0  35248  signstfveq0  35253  breprexplema  35306  breprexp  35309  circlevma  35318  circlemethhgt  35319  onf1oracwevd  35972  cvmliftlem5  36141  cvmliftlem7  36143  cvmliftlem10  36146  cvmliftlem13  36148  satefv  36266  mclsval  36415  rdgprc0  36648  dfrdg2  36650  bj-finsumval0  38300  rdgeqoa  38387  finxpeq2  38404  finxpreclem6  38413  finxpsuclem  38414  sdclem2  38770  ldualvsub  40306  ldualvsubval  40308  isopos  40331  polfvalN  41055  psubclsetN  41087  docaffvalN  42272  docafvalN  42273  djaffvalN  42284  djafvalN  42285  dihffval  42381  dihfval  42382  dochffval  42500  dochfval  42501  djhffval  42547  djhfval  42548  islpolN  42634  lcdfval  42739  lcdval  42740  lcdvsub  42768  lcdvsubval  42769  mapdffval  42777  mapdfval  42778  hdmap1fval  42947  hdmapfval  42978  hgmapfval  43037  hdmapglem7  43080  hlhilset  43085  aks6d1c1p1  43251  evlselv  43711  prjspnnormval  43753  0prjspnrel  43757  ismrc  43806  rmxfval  44005  rmyfval  44006  aomclem8  44157  hbt  44226  elmnc  44232  mncn0  44235  aaitgo  44258  clsk1independent  45140  binomcxp  45435  limciccioolb  46727  limcicciooub  46741  ioccncflimc  46989  icocncflimc  46993  dvnprodlem2  47051  dvnprodlem3  47052  dirkercncflem3  47209  fourierdlem32  47243  etransclem32  47370  etransclem44  47382  etransclem46  47384  etransc  47387  ovnsubaddlem1  47674  ovnsubaddlem2  47675  ovnsubadd  47676  hoidmvlelem4  47702  hoidmvlelem5  47703  hspmbl  47733  vonioo  47786  vonicc  47789  afveq12d  48297  iccelpart  48609  nnsum3primesprm  48982  funcringcsetcALTV2lem7  49487  funcringcsetcALTV2lem9  49489  funcringcsetclem7ALTV  49510  funcringcsetclem9ALTV  49512  cofu1a  50303  cofu2a  50304  cofid1  50324  cofid2  50325  uptr2  50431  swapfida  50496  cofuswapf2  50511  fuco21  50552  fuco23  50557  fucoid  50564  fucoaltvallem  50586  postcof2  50594  opf2  50635  oppfdiag1  50643  oppfdiag  50645  termolmd  50947