Theorem 2fveq3 6872

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 6867	. 2 ⊢ (𝐴 = 𝐵 → (𝐺‘𝐴) = (𝐺‘𝐵))
2	1	fveq2d 6871	1 ⊢ (𝐴 = 𝐵 → (𝐹‘(𝐺‘𝐴)) = (𝐹‘(𝐺‘𝐵)))

Syntax hints:   → wi 4   = wceq 1560  ‘cfv 6521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6477  df-fv 6529

This theorem is referenced by:  nvocnv  7265  2fvcoidd  7281  caofinvl  7692  oteqimp  7989  el2xptp0  8017  sbcoteq1a  8032  frpoins3xp3g  8121  xpord3lem  8129  seqomlem1  8421  xpmapen  9117  cnfcom  9655  updjudhcoinlf  9890  updjudhcoinrg  9891  acndom  10007  fodomacn  10012  alephcard  10026  iunfictbso  10070  ackbij2lem2  10195  axcc2  10394  axdc3lem2  10408  axdc3  10411  axdc4lem  10412  pwcfsdom  10541  pwfseqlem1  10616  pwfseqlem2  10617  rankcf  10735  recrecnq  10925  om2uzrdg  13969  uzrdgfni  13971  seqhomo  14062  hashf1  14470  seqcoll  14477  splval  14764  splcl  14765  o1co  15613  iseralt  15712  fsumf1o  15750  fsumrelem  15835  iserabs  15843  cvgcmpce  15846  supcvg  15886  explecnv  15895  cvgrat  15913  fprodf1o  15976  ruclem8  16269  ruclem9  16270  alginv  16609  algcvg  16610  algcvga  16613  iserodd  16871  prdsbasprj  17501  prdsplusgfval  17503  prdsmulrfval  17505  prdsvscafval  17509  prdsbas3  17510  prdsdsval2  17513  xpsle  17609  funcf2  17901  funcid  17903  funcpropd  17935  yonedalem3b  18311  yoniso  18317  prdsinvlem  19091  efgredlemd  19784  efgred  19788  dprdcntz  20050  ablfaclem3  20129  iscss  21735  prdsinvgd2  21794  evlslem1  22135  m1detdiag  22657  m2detleib  22691  cramerlem1  22747  pmatcoe1fsupp  22761  mat2pmatfval  22783  cpmadugsumlemF  22936  cpmadugsumfi  22937  cpmadumatpoly  22943  chcoeffeqlem  22945  cayhamlem3  22947  cayleyhamilton  22950  ptcld  23673  ptcldmpt  23674  dfac14  23678  alexsubALTlem1  24107  iscusp  24358  imasdsf1olem  24433  xpsdsval  24441  prdsxmslem2  24589  nmolb2d  24778  nmoi  24788  nmoleub2lem2  25178  nmoleub3  25181  caubl  25370  caublcls  25371  bcthlem4  25389  ovollb2lem  25550  ovollb2  25551  ovoliunlem1  25564  ovoliunlem2  25565  ovolshftlem2  25572  ovolscalem2  25576  ovolicc2lem1  25579  ovolicc2lem3  25581  ovolicc2lem4  25582  ovolicc2lem5  25583  ovolicc2  25584  voliunlem3  25614  voliun  25616  volsup  25618  ioombl1  25624  ovolfs2  25633  ioorinv  25638  uniioombllem2  25645  uniioombllem3  25647  uniioombllem4  25648  uniioombllem6  25650  dyadmbl  25662  mbflim  25730  itg2seq  25804  itg2monolem1  25812  itg2monolem2  25813  itg2monolem3  25814  itg2mono  25815  itg2i1fseq2  25818  itg2addlem  25820  bddmulibl  25901  bddiblnc  25904  dvlipcn  26056  c1liplem1  26058  dvfsumabs  26085  ftc1a  26099  aannenlem2  26393  aalioulem4  26399  radcnvlem2  26477  radcnvlt2  26482  dvradcnv  26484  pserulm  26485  abelthlem5  26498  abelthlem8  26502  logcnlem5  26711  lgamgulmlem2  27094  lgamgulmlem6  27098  ftalem2  27138  ftalem3  27139  ftalem5  27141  ftalem7  27143  fta  27144  bposlem7  27354  bposlem9  27356  rpvmasumlem  27551  dchrisumlem1  27553  dchrisumlem2  27554  dchrisumlem3  27555  dchrisum  27556  dchrmusumlema  27557  dchrmusum2  27558  dchrvmasumlem1  27559  dchrvmasum2lem  27560  dchrvmasumlema  27564  dchrvmasumiflem1  27565  dchrvmaeq0  27568  dchrisum0fval  27569  dchrisum0fmul  27570  dchrisum0ff  27571  dchrisum0flblem1  27572  dchrisum0re  27577  dchrisum0lema  27578  dchrisum0lem1b  27579  dchrisum0lem2a  27581  dchrisum0lem2  27582  rpvmasum  27590  pntlemo  27671  leftval  27942  rightval  27943  addsval  28055  negbdaylem  28149  om2noseqrdg  28397  expsval  28518  ewlkinedg  29805  wkslem1  29808  wkslem2  29809  2wlklem  29866  wlkdlem2  29882  upgrwlkdvdelem  29936  crctcshwlkn0lem4  30013  crctcshwlkn0lem5  30014  wlksnwwlknvbij  30108  2wlkdlem10  30135  clwlkclwwlklem1  30201  clwlkclwwlklem2  30202  clwlkclwwlkfolem  30209  clwlkclwwlkfo  30211  clwlkclwwlkf1  30212  clwlkclwwlken  30214  clwlknf1oclwwlknlem2  30284  clwlknf1oclwwlkn  30286  3wlkdlem10  30371  eupthseg  30408  upgreupthseg  30411  eupth2lem3  30438  fusgreghash2wsp  30540  clwwlknonclwlknonf1o  30564  dlwwlknondlwlknonf1o  30567  nmosetn0  30968  nmoolb  30974  nmounbseqi  30980  nmobndseqi  30982  nmlno0lem  30996  nmlnoubi  30999  blocnilem  31007  ubthlem1  31073  ubthlem2  31074  ubthlem3  31075  ococ  31609  pjoc1  31637  chscllem2  31841  chscllem3  31842  pjinormi  31890  pjnorm  31927  pjpyth  31928  pjnel  31929  nmopsetn0  32068  nmfnsetn0  32081  nmoplb  32110  nmfnlb  32127  lnopunilem1  32213  elunop2  32216  nmcexi  32229  lnconi  32236  branmfn  32308  pjbdlni  32352  pjss2coi  32367  pjdifnormi  32370  cdj3lem2b  32640  cdj3i  32644  fsumiunle  33031  prodindf  33040  mgcmntco  33172  dfmgc2  33174  elrgspnsubrunlem2  33429  deg1prod  33779  psrmonprod  33849  vietadeg1  33875  vietalem  33876  vieta  33877  ismntoplly  34322  esumiun  34391  sitgval  34629  signstf0  34862  hgt750lemg  34948  onvf1odlem4  35449  subfacp1lem4  35533  cvmliftlem3  35637  cvmliftlem15  35648  satfv0fvfmla0  35763  msubvrs  35910  sinccvg  36023  iprodefisumlem  36090  opnregcld  36690  cldregopn  36691  unblimceq0lem  36944  unbdqndv2  36949  bj-inftyexpitaudisj  37697  poimirlem5  38124  poimirlem6  38125  poimirlem7  38126  poimirlem8  38127  poimirlem10  38129  poimirlem11  38130  poimirlem12  38131  poimirlem13  38132  poimirlem14  38133  poimirlem15  38134  poimirlem16  38135  poimirlem17  38136  poimirlem18  38137  poimirlem19  38138  poimirlem20  38139  poimirlem21  38140  poimirlem22  38141  poimirlem27  38146  poimirlem32  38151  mblfinlem2  38157  ovoliunnfl  38161  ex-ovoliunnfl  38162  ftc1anclem6  38197  prdsbnd2  38294  lflnegcl  39699  oposlem  39806  pmapglb2N  40395  polatN  40555  ispsubclN  40561  ispsubcl2N  40571  cdlemg16zz  41284  cdlemg40  41341  tendotp  41385  dvhvscacbv  41722  dvhvscaval  41723  dochlkr  42009  dochkrshp  42010  dochkrshp4  42013  djhfval  42021  lpolsatN  42112  lpolpolsatN  42113  lclkrlem2e  42135  lcfrvalsnN  42165  lcfrlem27  42193  lcfrlem37  42203  lcfr  42209  mapdordlem1a  42258  mapdordlem1  42260  mapdrvallem3  42270  mapdrval  42271  mapd0  42289  hdmap1vallem  42421  hdmap1cbv  42426  hdmapfval  42451  hgmapfval  42510  hgmapvv  42550  aks6d1c1p5  42729  aks6d1c1  42733  aks6d1c5lem3  42754  deg1gprod  42757  aks6d1c6lem1  42787  aks6d1c7lem3  42799  readvcot  42973  ismrcd2  43280  ismrc  43282  hbt  43707  mpaaval  43728  cantnfub  43898  ntrclsk4  44648  dvgrat  44888  mccllem  46173  mccl  46174  climsuse  46184  limsupref  46259  climbddf  46261  dvbdfbdioolem2  46503  dvbdfbdioo  46504  ioodvbdlimc1lem1  46505  ioodvbdlimc1lem2  46506  ioodvbdlimc1  46507  ioodvbdlimc2lem  46508  ioodvbdlimc2  46509  stirlinglem4  46651  stirlinglem11  46658  stirlinglem12  46659  stirlinglem13  46660  stirlinglem14  46661  etransclem48  46856  ioorrnopn  46879  ioorrnopnxr  46881  voliunsge0lem  47046  meaiuninclem  47054  meaiuninc  47055  meaiunincf  47057  meaiuninc3v  47058  meaiuninc3  47059  meaiininc  47061  omeiunle  47091  omeiunltfirp  47093  caratheodorylem1  47100  vonval  47114  ovn0lem  47139  ovnsubaddlem1  47144  ovnsubaddlem2  47145  ovnsubadd  47146  hoidmvlelem5  47173  ovnhoilem2  47176  hoiqssbl  47199  hspmbllem2  47201  hspmbl  47203  opnvonmbllem2  47207  ovnsubadd2lem  47219  ovolval4lem2  47224  ovolval4  47225  ovolval5lem2  47227  ovolval5lem3  47228  ovnovollem1  47230  ovnovollem2  47231  vonioolem2  47255  vonicclem2  47258  fargshiftfva  48049  grimuhgr  48509  grimcnv  48510  grimco  48511  uhgrimedgi  48512  isuspgrim0lem  48515  isuspgrim0  48516  upgrimwlklem3  48521  upgrimwlklem5  48523  upgrimtrls  48528  gricushgr  48539  cycldlenngric  48550  uhgrimisgrgriclem  48552  clnbgrgrimlem  48555  clnbgrgrim  48556  grimedg  48557  uspgrlimlem3  48612  lincop  49030  lcoop  49033  ldepsnlinc  49130  lines  49353  oppcinito  49856  oppctermo  49857  fucoid  49969