Theorem 2fveq3 6890

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

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

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 2737

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 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548

This theorem is used by:  nvocnv  7288  2fvcoidd  7304  caofinvl  7716  oteqimp  8011  el2xptp0  8039  sbcoteq1a  8054  frpoins3xp3g  8143  xpord3lem  8151  seqomlem1  8443  xpmapen  9140  cnfcom  9676  updjudhcoinlf  9934  updjudhcoinrg  9935  acndom  10051  fodomacn  10056  alephcard  10070  iunfictbso  10114  ackbij2lem2  10238  axcc2  10436  axdc3lem2  10450  axdc3  10453  axdc4lem  10454  pwcfsdom  10585  pwfseqlem1  10660  pwfseqlem2  10661  rankcf  10779  recrecnq  10969  om2uzrdg  14012  uzrdgfni  14014  seqhomo  14105  hashf1  14514  seqcoll  14521  splval  14812  splcl  14813  o1co  15663  iseralt  15762  fsumf1o  15799  fsumrelem  15884  iserabs  15892  cvgcmpce  15895  supcvg  15935  explecnv  15944  cvgrat  15962  fprodf1o  16025  ruclem8  16317  ruclem9  16318  alginv  16657  algcvg  16658  algcvga  16661  iserodd  16919  prdsbasprj  17549  prdsplusgfval  17551  prdsmulrfval  17553  prdsvscafval  17557  prdsbas3  17558  prdsdsval2  17561  xpsle  17657  funcf2  17949  funcid  17951  funcpropd  17983  yonedalem3b  18359  yoniso  18365  prdsinvlem  19161  efgredlemd  19860  efgred  19864  dprdcntz  20126  ablfaclem3  20205  iscss  21885  prdsinvgd2  21944  evlslem1  22285  m1detdiag  22806  m2detleib  22840  cramerlem1  22896  pmatcoe1fsupp  22910  mat2pmatfval  22932  cpmadugsumlemF  23085  cpmadugsumfi  23086  cpmadumatpoly  23092  chcoeffeqlem  23094  cayhamlem3  23096  cayleyhamilton  23099  ptcld  23823  ptcldmpt  23824  dfac14  23828  alexsubALTlem1  24257  iscusp  24508  imasdsf1olem  24583  xpsdsval  24591  prdsxmslem2  24739  nmolb2d  24928  nmoi  24938  nmoleub2lem2  25328  nmoleub3  25331  caubl  25520  caublcls  25521  bcthlem4  25539  ovollb2lem  25700  ovollb2  25701  ovoliunlem1  25714  ovoliunlem2  25715  ovolshftlem2  25722  ovolscalem2  25726  ovolicc2lem1  25729  ovolicc2lem3  25731  ovolicc2lem4  25732  ovolicc2lem5  25733  ovolicc2  25734  voliunlem3  25764  voliun  25766  volsup  25768  ioombl1  25774  ovolfs2  25783  ioorinv  25788  uniioombllem2  25795  uniioombllem3  25797  uniioombllem4  25798  uniioombllem6  25800  dyadmbl  25812  mbflim  25880  itg2seq  25954  itg2monolem1  25962  itg2monolem2  25963  itg2monolem3  25964  itg2mono  25965  itg2i1fseq2  25968  itg2addlem  25970  bddmulibl  26051  bddiblnc  26054  dvlipcn  26206  c1liplem1  26208  dvfsumabs  26235  ftc1a  26249  aannenlem2  26545  aalioulem4  26551  radcnvlem2  26630  radcnvlt2  26635  dvradcnv  26637  pserulm  26638  abelthlem5  26651  abelthlem8  26655  logcnlem5  26864  lgamgulmlem2  27247  lgamgulmlem6  27251  ftalem2  27291  ftalem3  27292  ftalem5  27294  ftalem7  27296  fta  27297  bposlem7  27507  bposlem9  27509  rpvmasumlem  27704  dchrisumlem1  27706  dchrisumlem2  27707  dchrisumlem3  27708  dchrisum  27709  dchrmusumlema  27710  dchrmusum2  27711  dchrvmasumlem1  27712  dchrvmasum2lem  27713  dchrvmasumlema  27717  dchrvmasumiflem1  27718  dchrvmaeq0  27721  dchrisum0fval  27722  dchrisum0fmul  27723  dchrisum0ff  27724  dchrisum0flblem1  27725  dchrisum0re  27730  dchrisum0lema  27731  dchrisum0lem1b  27732  dchrisum0lem2a  27734  dchrisum0lem2  27735  rpvmasum  27743  pntlemo  27824  leftval  28095  rightval  28096  addsval  28208  negbdaylem  28302  om2noseqrdg  28550  expsval  28671  ewlkinedg  30014  wkslem1  30017  wkslem2  30018  2wlklem  30075  wlkdlem2  30091  upgrwlkdvdelem  30151  crctcshwlkn0lem4  30231  crctcshwlkn0lem5  30232  wlksnwwlknvbij  30326  2wlkdlem10  30353  clwlkclwwlklem1  30419  clwlkclwwlklem2  30420  clwlkclwwlkfolem  30427  clwlkclwwlkfo  30429  clwlkclwwlkf1  30430  clwlkclwwlken  30432  clwlknf1oclwwlknlem2  30502  clwlknf1oclwwlkn  30504  3wlkdlem10  30593  eupthseg  30630  upgreupthseg  30633  eupth2lem3  30660  fusgreghash2wsp  30762  clwwlknonclwlknonf1o  30786  dlwwlknondlwlknonf1o  30789  nmosetn0  31190  nmoolb  31196  nmounbseqi  31202  nmobndseqi  31204  nmlno0lem  31218  nmlnoubi  31221  blocnilem  31229  ubthlem1  31295  ubthlem2  31296  ubthlem3  31297  ococ  31831  pjoc1  31859  chscllem2  32063  chscllem3  32064  pjinormi  32112  pjnorm  32149  pjpyth  32150  pjnel  32151  nmopsetn0  32290  nmfnsetn0  32303  nmoplb  32332  nmfnlb  32349  lnopunilem1  32435  elunop2  32438  nmcexi  32451  lnconi  32458  branmfn  32530  pjbdlni  32574  pjss2coi  32589  pjdifnormi  32592  cdj3lem2b  32862  cdj3i  32866  fsumiunle  33245  prodindf  33254  mgcmntco  33380  dfmgc2  33382  elrgspnsubrunlem2  33634  deg1prod  33939  psrmonprod  34008  vietadeg1  34034  vietalem  34035  vieta  34036  ismntoplly  34481  esumiun  34550  sitgval  34789  signstf0  35022  hgt750lemg  35108  onvf1odlem4  35649  subfacp1lem4  35714  cvmliftlem3  35818  cvmliftlem15  35829  satfv0fvfmla0  35944  msubvrs  36091  sinccvg  36204  iprodefisumlem  36271  opnregcld  36900  cldregopn  36901  unblimceq0lem  37154  unbdqndv2  37159  bj-inftyexpitaudisj  37908  poimirlem5  38335  poimirlem6  38336  poimirlem7  38337  poimirlem8  38338  poimirlem10  38340  poimirlem11  38341  poimirlem12  38342  poimirlem13  38343  poimirlem14  38344  poimirlem15  38345  poimirlem16  38346  poimirlem17  38347  poimirlem18  38348  poimirlem19  38349  poimirlem20  38350  poimirlem21  38351  poimirlem22  38352  poimirlem27  38357  poimirlem32  38362  mblfinlem2  38368  ovoliunnfl  38372  ex-ovoliunnfl  38373  ftc1anclem6  38408  prdsbnd2  38506  lflnegcl  39909  oposlem  40016  pmapglb2N  40605  polatN  40765  ispsubclN  40771  ispsubcl2N  40781  cdlemg16zz  41494  cdlemg40  41551  tendotp  41595  dvhvscacbv  41932  dvhvscaval  41933  dochlkr  42219  dochkrshp  42220  dochkrshp4  42223  djhfval  42231  lpolsatN  42322  lpolpolsatN  42323  lclkrlem2e  42345  lcfrvalsnN  42375  lcfrlem27  42403  lcfrlem37  42413  lcfr  42419  mapdordlem1a  42468  mapdordlem1  42470  mapdrvallem3  42480  mapdrval  42481  mapd0  42499  hdmap1vallem  42631  hdmap1cbv  42636  hdmapfval  42661  hgmapfval  42720  hgmapvv  42760  aks6d1c1p5  42939  aks6d1c1  42943  aks6d1c5lem3  42964  deg1gprod  42967  aks6d1c6lem1  42997  aks6d1c7lem3  43009  readvcot  43185  ismrcd2  43490  ismrc  43492  hbt  43917  mpaaval  43938  cantnfub  44108  ntrclsk4  44858  dvgrat  45082  mccllem  46373  mccl  46374  climsuse  46384  limsupref  46459  climbddf  46461  dvbdfbdioolem2  46703  dvbdfbdioo  46704  ioodvbdlimc1lem1  46705  ioodvbdlimc1lem2  46706  ioodvbdlimc1  46707  ioodvbdlimc2lem  46708  ioodvbdlimc2  46709  stirlinglem4  46851  stirlinglem11  46858  stirlinglem12  46859  stirlinglem13  46860  stirlinglem14  46861  etransclem48  47056  ioorrnopn  47079  ioorrnopnxr  47081  voliunsge0lem  47246  meaiuninclem  47254  meaiuninc  47255  meaiunincf  47257  meaiuninc3v  47258  meaiuninc3  47259  meaiininc  47261  omeiunle  47291  omeiunltfirp  47293  caratheodorylem1  47300  vonval  47314  ovn0lem  47339  ovnsubaddlem1  47344  ovnsubaddlem2  47345  ovnsubadd  47346  hoidmvlelem5  47373  ovnhoilem2  47376  hoiqssbl  47399  hspmbllem2  47401  hspmbl  47403  opnvonmbllem2  47407  ovnsubadd2lem  47419  ovolval4lem2  47424  ovolval4  47425  ovolval5lem2  47427  ovolval5lem3  47428  ovnovollem1  47430  ovnovollem2  47431  vonioolem2  47455  vonicclem2  47458  fargshiftfva  48252  grimuhgr  48712  grimcnv  48713  grimco  48714  uhgrimedgi  48715  isuspgrim0lem  48718  isuspgrim0  48719  upgrimwlklem3  48724  upgrimwlklem5  48726  upgrimtrls  48731  gricushgr  48742  cycldlenngric  48753  uhgrimisgrgriclem  48755  clnbgrgrimlem  48758  clnbgrgrim  48759  grimedg  48760  uspgrlimlem3  48815  lincop  49247  lcoop  49250  ldepsnlinc  49347  lines  49570  oppcinito  50072  oppctermo  50073  fucoid  50185