Theorem 2fveq3 6827

Description: Equality theorem for nested function values. (Contributed by AV, 14-Aug-2022.)

Assertion

Ref	Expression
2fveq3	⊢ (𝐴 = 𝐵 → (𝐹‘(𝐺‘𝐴)) = (𝐹‘(𝐺‘𝐵)))

Proof of Theorem 2fveq3

Step	Hyp	Ref	Expression
1		fveq2 6822	. 2 ⊢ (𝐴 = 𝐵 → (𝐺‘𝐴) = (𝐺‘𝐵))
2	1	fveq2d 6826	1 ⊢ (𝐴 = 𝐵 → (𝐹‘(𝐺‘𝐴)) = (𝐹‘(𝐺‘𝐵)))

Syntax hints:   → wi 4   = wceq 1541  ‘cfv 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489

This theorem is referenced by:  nvocnv  7215  2fvcoidd  7231  caofinvl  7642  oteqimp  7940  el2xptp0  7968  sbcoteq1a  7983  frpoins3xp3g  8071  xpord3lem  8079  seqomlem1  8369  xpmapen  9058  cnfcom  9590  updjudhcoinlf  9825  updjudhcoinrg  9826  acndom  9942  fodomacn  9947  alephcard  9961  iunfictbso  10005  ackbij2lem2  10130  axcc2  10328  axdc3lem2  10342  axdc3  10345  axdc4lem  10346  pwcfsdom  10474  pwfseqlem1  10549  pwfseqlem2  10550  rankcf  10668  recrecnq  10858  om2uzrdg  13863  uzrdgfni  13865  seqhomo  13956  hashf1  14364  seqcoll  14371  splval  14658  splcl  14659  o1co  15493  iseralt  15592  fsumf1o  15630  fsumrelem  15714  iserabs  15722  cvgcmpce  15725  supcvg  15763  explecnv  15772  cvgrat  15790  fprodf1o  15853  ruclem8  16146  ruclem9  16147  alginv  16486  algcvg  16487  algcvga  16490  iserodd  16747  prdsbasprj  17376  prdsplusgfval  17378  prdsmulrfval  17380  prdsvscafval  17384  prdsbas3  17385  prdsdsval2  17388  xpsle  17483  funcf2  17775  funcid  17777  funcpropd  17809  yonedalem3b  18185  yoniso  18191  prdsinvlem  18962  efgredlemd  19656  efgred  19660  dprdcntz  19922  ablfaclem3  20001  iscss  21620  prdsinvgd2  21679  evlslem1  22017  m1detdiag  22512  m2detleib  22546  cramerlem1  22602  pmatcoe1fsupp  22616  mat2pmatfval  22638  cpmadugsumlemF  22791  cpmadugsumfi  22792  cpmadumatpoly  22798  chcoeffeqlem  22800  cayhamlem3  22802  cayleyhamilton  22805  ptcld  23528  ptcldmpt  23529  dfac14  23533  alexsubALTlem1  23962  iscusp  24213  imasdsf1olem  24288  xpsdsval  24296  prdsxmslem2  24444  nmolb2d  24633  nmoi  24643  nmoleub2lem2  25043  nmoleub3  25046  caubl  25235  caublcls  25236  bcthlem4  25254  ovollb2lem  25416  ovollb2  25417  ovoliunlem1  25430  ovoliunlem2  25431  ovolshftlem2  25438  ovolscalem2  25442  ovolicc2lem1  25445  ovolicc2lem3  25447  ovolicc2lem4  25448  ovolicc2lem5  25449  ovolicc2  25450  voliunlem3  25480  voliun  25482  volsup  25484  ioombl1  25490  ovolfs2  25499  ioorinv  25504  uniioombllem2  25511  uniioombllem3  25513  uniioombllem4  25514  uniioombllem6  25516  dyadmbl  25528  mbflim  25596  itg2seq  25670  itg2monolem1  25678  itg2monolem2  25679  itg2monolem3  25680  itg2mono  25681  itg2i1fseq2  25684  itg2addlem  25686  bddmulibl  25767  bddiblnc  25770  dvlipcn  25926  c1liplem1  25928  dvfsumabs  25956  ftc1a  25971  aannenlem2  26264  aalioulem4  26270  radcnvlem2  26350  radcnvlt2  26355  dvradcnv  26357  pserulm  26358  abelthlem5  26372  abelthlem8  26376  logcnlem5  26582  lgamgulmlem2  26967  lgamgulmlem6  26971  ftalem2  27011  ftalem3  27012  ftalem5  27014  ftalem7  27016  fta  27017  bposlem7  27228  bposlem9  27230  rpvmasumlem  27425  dchrisumlem1  27427  dchrisumlem2  27428  dchrisumlem3  27429  dchrisum  27430  dchrmusumlema  27431  dchrmusum2  27432  dchrvmasumlem1  27433  dchrvmasum2lem  27434  dchrvmasumlema  27438  dchrvmasumiflem1  27439  dchrvmaeq0  27442  dchrisum0fval  27443  dchrisum0fmul  27444  dchrisum0ff  27445  dchrisum0flblem1  27446  dchrisum0re  27451  dchrisum0lema  27452  dchrisum0lem1b  27453  dchrisum0lem2a  27455  dchrisum0lem2  27456  rpvmasum  27464  pntlemo  27545  leftval  27804  rightval  27805  addsval  27905  negsbdaylem  27998  om2noseqrdg  28234  expsval  28348  ewlkinedg  29583  wkslem1  29586  wkslem2  29587  2wlklem  29644  wlkdlem2  29660  upgrwlkdvdelem  29714  crctcshwlkn0lem4  29791  crctcshwlkn0lem5  29792  wlksnwwlknvbij  29886  2wlkdlem10  29913  clwlkclwwlklem1  29979  clwlkclwwlklem2  29980  clwlkclwwlkfolem  29987  clwlkclwwlkfo  29989  clwlkclwwlkf1  29990  clwlkclwwlken  29992  clwlknf1oclwwlknlem2  30062  clwlknf1oclwwlkn  30064  3wlkdlem10  30149  eupthseg  30186  upgreupthseg  30189  eupth2lem3  30216  fusgreghash2wsp  30318  clwwlknonclwlknonf1o  30342  dlwwlknondlwlknonf1o  30345  nmosetn0  30745  nmoolb  30751  nmounbseqi  30757  nmobndseqi  30759  nmlno0lem  30773  nmlnoubi  30776  blocnilem  30784  ubthlem1  30850  ubthlem2  30851  ubthlem3  30852  ococ  31386  pjoc1  31414  chscllem2  31618  chscllem3  31619  pjinormi  31667  pjnorm  31704  pjpyth  31705  pjnel  31706  nmopsetn0  31845  nmfnsetn0  31858  nmoplb  31887  nmfnlb  31904  lnopunilem1  31990  elunop2  31993  nmcexi  32006  lnconi  32013  branmfn  32085  pjbdlni  32129  pjss2coi  32144  pjdifnormi  32147  cdj3lem2b  32417  cdj3i  32421  fsumiunle  32812  prodindf  32844  mgcmntco  32975  dfmgc2  32977  elrgspnsubrunlem2  33215  ismntoplly  34038  esumiun  34107  sitgval  34345  signstf0  34581  hgt750lemg  34667  onvf1odlem4  35150  subfacp1lem4  35227  cvmliftlem3  35331  cvmliftlem15  35342  satfv0fvfmla0  35457  msubvrs  35604  sinccvg  35717  iprodefisumlem  35784  opnregcld  36374  cldregopn  36375  unblimceq0lem  36550  unbdqndv2  36555  bj-inftyexpitaudisj  37249  poimirlem5  37675  poimirlem6  37676  poimirlem7  37677  poimirlem8  37678  poimirlem10  37680  poimirlem11  37681  poimirlem12  37682  poimirlem13  37683  poimirlem14  37684  poimirlem15  37685  poimirlem16  37686  poimirlem17  37687  poimirlem18  37688  poimirlem19  37689  poimirlem20  37690  poimirlem21  37691  poimirlem22  37692  poimirlem27  37697  poimirlem32  37702  mblfinlem2  37708  ovoliunnfl  37712  ex-ovoliunnfl  37713  ftc1anclem6  37748  prdsbnd2  37845  lflnegcl  39184  oposlem  39291  pmapglb2N  39880  polatN  40040  ispsubclN  40046  ispsubcl2N  40056  cdlemg16zz  40769  cdlemg40  40826  tendotp  40870  dvhvscacbv  41207  dvhvscaval  41208  dochlkr  41494  dochkrshp  41495  dochkrshp4  41498  djhfval  41506  lpolsatN  41597  lpolpolsatN  41598  lclkrlem2e  41620  lcfrvalsnN  41650  lcfrlem27  41678  lcfrlem37  41688  lcfr  41694  mapdordlem1a  41743  mapdordlem1  41745  mapdrvallem3  41755  mapdrval  41756  mapd0  41774  hdmap1vallem  41906  hdmap1cbv  41911  hdmapfval  41936  hgmapfval  41995  hgmapvv  42035  aks6d1c1p5  42215  aks6d1c1  42219  aks6d1c5lem3  42240  deg1gprod  42243  aks6d1c6lem1  42273  aks6d1c7lem3  42285  readvcot  42467  ismrcd2  42802  ismrc  42804  hbt  43233  mpaaval  43254  cantnfub  43424  ntrclsk4  44175  dvgrat  44415  mccllem  45707  mccl  45708  climsuse  45718  limsupref  45793  climbddf  45795  dvbdfbdioolem2  46037  dvbdfbdioo  46038  ioodvbdlimc1lem1  46039  ioodvbdlimc1lem2  46040  ioodvbdlimc1  46041  ioodvbdlimc2lem  46042  ioodvbdlimc2  46043  stirlinglem4  46185  stirlinglem11  46192  stirlinglem12  46193  stirlinglem13  46194  stirlinglem14  46195  etransclem48  46390  ioorrnopn  46413  ioorrnopnxr  46415  voliunsge0lem  46580  meaiuninclem  46588  meaiuninc  46589  meaiunincf  46591  meaiuninc3v  46592  meaiuninc3  46593  meaiininc  46595  omeiunle  46625  omeiunltfirp  46627  caratheodorylem1  46634  vonval  46648  ovn0lem  46673  ovnsubaddlem1  46678  ovnsubaddlem2  46679  ovnsubadd  46680  hoidmvlelem5  46707  ovnhoilem2  46710  hoiqssbl  46733  hspmbllem2  46735  hspmbl  46737  opnvonmbllem2  46741  ovnsubadd2lem  46753  ovolval4lem2  46758  ovolval4  46759  ovolval5lem2  46761  ovolval5lem3  46762  ovnovollem1  46764  ovnovollem2  46765  vonioolem2  46789  vonicclem2  46792  fargshiftfva  47553  grimuhgr  47997  grimcnv  47998  grimco  47999  uhgrimedgi  48000  isuspgrim0lem  48003  isuspgrim0  48004  upgrimwlklem3  48009  upgrimwlklem5  48011  upgrimtrls  48016  gricushgr  48027  cycldlenngric  48038  uhgrimisgrgriclem  48040  clnbgrgrimlem  48043  clnbgrgrim  48044  grimedg  48045  uspgrlimlem3  48100  lincop  48519  lcoop  48522  ldepsnlinc  48619  lines  48842  oppcinito  49346  oppctermo  49347  fucoid  49459