Theorem fveq12d 6895

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

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 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-iota 6499  df-fv 6551

This theorem is used by:  nffvd  6900  fvmpopr2d  7585  tfrlem3a  8372  resixpfo  8943  cantnfval  9647  cantnfres  9656  fseqenlem1  10027  fseqenlem2  10028  dfac12lem1  10146  dfac12lem2  10147  dfac12r  10149  hsmexlem2  10429  ttukeylem3  10513  ttukey2g  10518  seq1  14070  expval  14119  lsw  14621  ccatfval  14630  swrdval  14703  splfv2a  14817  revval  14821  relexpsucnnr  15088  relexp1g  15089  seqshft  15148  climshft2  15659  fprodser  16029  imasval  17590  funcid  17952  funcco  17953  funcoppc  17957  funcres  17978  nati  18040  funcestrcsetclem7  18227  funcestrcsetclem9  18229  funcsetcestrclem7  18242  funcsetcestrclem9  18244  evlf2  18299  evlf1  18301  evlfcl  18303  uncf2  18318  hofcl  18340  yonedalem21  18354  yonedalem3a  18355  yonedalem4a  18356  yonedalem4b  18357  yonedalem22  18359  yonedalem3  18361  yonedainv  18362  p0val  18506  p1val  18507  gsumvalx  18763  gsumpropd  18765  gsumval2a  18772  gsumsgrpccat  18930  prdsinvlem  19146  mulgfval  19166  mulgfvalALT  19167  mulgval  19168  mulgnndir  19200  mulgpropd  19213  cntrval  19420  efgsf  19830  efgsval  19832  issrngd  20995  rlmval  21349  chrval  21710  znval  21722  isphl  21815  isphld  21841  phlpropd  21842  cssval  21869  prdsinvgd2  21929  islindf  21999  evlseu  22271  evlval  22288  selvffval  22306  selvval  22308  evls1fval  22516  evl1varpw  22558  madetsumid  22655  madufval  22831  smadiadetr  22869  decpmatval0  22958  chpmatfval  23024  isperf  23345  dfac14  23812  xkohmeo  24009  flffval  24183  fcfval  24227  cnextfval  24256  tsmsval2  24324  tsmspropd  24326  tngngp  24848  tngngp3  24850  isnlm  24869  sranlm  24878  cnncvsabsnegdemo  25361  ovoliunlem1  25698  ovoliunlem2  25699  limcfval  26068  dvfval  26093  dvreslem  26105  dvaddbr  26134  dvmulbr  26135  isuc1p  26335  ismon1p  26337  mon1pid  26348  q1pval  26349  dgreq0  26459  vieta1lem2  26509  vieta1  26510  basellem5  27286  lgsval  27502  lgsneg  27522  seqseq123d  28516  israg  29014  iswlkon  30042  wlkres  30055  wlkp1lem3  30060  wlkp1lem6  30063  isclwlk  30159  iscrct  30176  iscycl  30177  eupth2eucrct  30605  dipfval  31091  prodindf  33219  splfv3  33309  cycpmco2lem5  33481  cycpmco2lem6  33482  idlsrgval  33824  m1pmeq  33906  mplvrpmfgalem  33965  mplvrpmga  33966  mplvrpmmhm  33967  mplvrpmrhm  33968  issply  33982  esplyval  33983  esplyind  33996  vieta  34001  extdgval  34074  fldextrspundgle  34099  minplyval  34126  constrcon  34195  2sqr3minply  34201  lmatfval  34235  lmat22e11  34239  rrhval  34417  xrhval  34439  brae  34663  braew  34664  sitmval  34771  sseqval  34810  fibp1  34823  elprob  34831  signsvtn0  34989  signstfvneq0  34991  signstfveq0  34996  breprexplema  35049  breprexp  35052  circlevma  35061  circlemethhgt  35062  cvmliftlem5  35802  cvmliftlem7  35804  cvmliftlem10  35807  cvmliftlem13  35809  satefv  35927  mclsval  36076  rdgprc0  36304  dfrdg2  36306  bj-finsumval0  37970  rdgeqoa  38057  finxpeq2  38074  finxpreclem6  38083  finxpsuclem  38084  sdclem2  38434  ldualvsub  39970  ldualvsubval  39972  isopos  39995  polfvalN  40719  psubclsetN  40751  docaffvalN  41936  docafvalN  41937  djaffvalN  41948  djafvalN  41949  dihffval  42045  dihfval  42046  dochffval  42164  dochfval  42165  djhffval  42211  djhfval  42212  islpolN  42298  lcdfval  42403  lcdval  42404  lcdvsub  42432  lcdvsubval  42433  mapdffval  42441  mapdfval  42442  hdmap1fval  42611  hdmapfval  42642  hgmapfval  42701  hdmapglem7  42744  hlhilset  42749  aks6d1c1p1  42915  evlselv  43362  0prjspnrel  43400  ismrc  43473  rmxfval  43672  rmyfval  43673  aomclem8  43829  hbt  43898  elmnc  43904  mncn0  43907  aaitgo  43930  clsk1independent  44813  binomcxp  45108  limciccioolb  46378  limcicciooub  46392  ioccncflimc  46640  icocncflimc  46644  dvnprodlem2  46702  dvnprodlem3  46703  dirkercncflem3  46860  fourierdlem32  46894  etransclem32  47021  etransclem44  47033  etransclem46  47035  etransc  47038  ovnsubaddlem1  47325  ovnsubaddlem2  47326  ovnsubadd  47327  hoidmvlelem4  47353  hoidmvlelem5  47354  hspmbl  47384  vonioo  47437  vonicc  47440  afveq12d  47911  iccelpart  48223  nnsum3primesprm  48596  funcringcsetcALTV2lem7  49102  funcringcsetcALTV2lem9  49104  funcringcsetclem7ALTV  49125  funcringcsetclem9ALTV  49127  cofu1a  49913  cofu2a  49914  cofid1  49933  cofid2  49934  uptr2  50040  swapfida  50099  cofuswapf2  50114  fuco21  50155  fuco23  50160  fucoid  50167  opf2  50225  oppfdiag1  50233  oppfdiag  50235  termolmd  50489