Theorem 2fveq3 6925

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

Syntax hints:   → wi 4   = wceq 1537  ‘cfv 6573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581

This theorem is referenced by:  nvocnv  7317  2fvcoidd  7333  caofinvl  7745  oteqimp  8049  el2xptp0  8077  sbcoteq1a  8092  frpoins3xp3g  8182  xpord3lem  8190  seqomlem1  8506  xpmapen  9211  cnfcom  9769  updjudhcoinlf  10001  updjudhcoinrg  10002  acndom  10120  fodomacn  10125  alephcard  10139  iunfictbso  10183  ackbij2lem2  10308  axcc2  10506  axdc3lem2  10520  axdc3  10523  axdc4lem  10524  pwcfsdom  10652  pwfseqlem1  10727  pwfseqlem2  10728  rankcf  10846  recrecnq  11036  om2uzrdg  14007  uzrdgfni  14009  seqhomo  14100  hashf1  14506  seqcoll  14513  splval  14799  splcl  14800  o1co  15632  iseralt  15733  fsumf1o  15771  fsumrelem  15855  iserabs  15863  cvgcmpce  15866  supcvg  15904  explecnv  15913  cvgrat  15931  fprodf1o  15994  ruclem8  16285  ruclem9  16286  alginv  16622  algcvg  16623  algcvga  16626  iserodd  16882  prdsbasprj  17532  prdsplusgfval  17534  prdsmulrfval  17536  prdsvscafval  17540  prdsbas3  17541  prdsdsval2  17544  xpsle  17639  funcf2  17932  funcid  17934  funcpropd  17967  yonedalem3b  18349  yoniso  18355  prdsinvlem  19089  efgredlemd  19786  efgred  19790  dprdcntz  20052  ablfaclem3  20131  iscss  21724  prdsinvgd2  21785  evlslem1  22129  m1detdiag  22624  m2detleib  22658  cramerlem1  22714  pmatcoe1fsupp  22728  mat2pmatfval  22750  cpmadugsumlemF  22903  cpmadugsumfi  22904  cpmadumatpoly  22910  chcoeffeqlem  22912  cayhamlem3  22914  cayleyhamilton  22917  ptcld  23642  ptcldmpt  23643  dfac14  23647  alexsubALTlem1  24076  iscusp  24329  imasdsf1olem  24404  xpsdsval  24412  prdsxmslem2  24563  nmolb2d  24760  nmoi  24770  nmoleub2lem2  25168  nmoleub3  25171  caubl  25361  caublcls  25362  bcthlem4  25380  ovollb2lem  25542  ovollb2  25543  ovoliunlem1  25556  ovoliunlem2  25557  ovolshftlem2  25564  ovolscalem2  25568  ovolicc2lem1  25571  ovolicc2lem3  25573  ovolicc2lem4  25574  ovolicc2lem5  25575  ovolicc2  25576  voliunlem3  25606  voliun  25608  volsup  25610  ioombl1  25616  ovolfs2  25625  ioorinv  25630  uniioombllem2  25637  uniioombllem3  25639  uniioombllem4  25640  uniioombllem6  25642  dyadmbl  25654  mbflim  25722  itg2seq  25797  itg2monolem1  25805  itg2monolem2  25806  itg2monolem3  25807  itg2mono  25808  itg2i1fseq2  25811  itg2addlem  25813  bddmulibl  25894  bddiblnc  25897  dvlipcn  26053  c1liplem1  26055  dvfsumabs  26083  ftc1a  26098  aannenlem2  26389  aalioulem4  26395  radcnvlem2  26475  radcnvlt2  26480  dvradcnv  26482  pserulm  26483  abelthlem5  26497  abelthlem8  26501  logcnlem5  26706  lgamgulmlem2  27091  lgamgulmlem6  27095  ftalem2  27135  ftalem3  27136  ftalem5  27138  ftalem7  27140  fta  27141  bposlem7  27352  bposlem9  27354  rpvmasumlem  27549  dchrisumlem1  27551  dchrisumlem2  27552  dchrisumlem3  27553  dchrisum  27554  dchrmusumlema  27555  dchrmusum2  27556  dchrvmasumlem1  27557  dchrvmasum2lem  27558  dchrvmasumlema  27562  dchrvmasumiflem1  27563  dchrvmaeq0  27566  dchrisum0fval  27567  dchrisum0fmul  27568  dchrisum0ff  27569  dchrisum0flblem1  27570  dchrisum0re  27575  dchrisum0lema  27576  dchrisum0lem1b  27577  dchrisum0lem2a  27579  dchrisum0lem2  27580  rpvmasum  27588  pntlemo  27669  leftval  27920  rightval  27921  addsval  28013  negsbdaylem  28106  om2noseqrdg  28328  expsval  28426  ewlkinedg  29640  wkslem1  29643  wkslem2  29644  2wlklem  29703  wlkdlem2  29719  upgrwlkdvdelem  29772  crctcshwlkn0lem4  29846  crctcshwlkn0lem5  29847  wlksnwwlknvbij  29941  2wlkdlem10  29968  clwlkclwwlklem1  30031  clwlkclwwlklem2  30032  clwlkclwwlkfolem  30039  clwlkclwwlkfo  30041  clwlkclwwlkf1  30042  clwlkclwwlken  30044  clwlknf1oclwwlknlem2  30114  clwlknf1oclwwlkn  30116  3wlkdlem10  30201  eupthseg  30238  upgreupthseg  30241  eupth2lem3  30268  fusgreghash2wsp  30370  clwwlknonclwlknonf1o  30394  dlwwlknondlwlknonf1o  30397  nmosetn0  30797  nmoolb  30803  nmounbseqi  30809  nmobndseqi  30811  nmlno0lem  30825  nmlnoubi  30828  blocnilem  30836  ubthlem1  30902  ubthlem2  30903  ubthlem3  30904  ococ  31438  pjoc1  31466  chscllem2  31670  chscllem3  31671  pjinormi  31719  pjnorm  31756  pjpyth  31757  pjnel  31758  nmopsetn0  31897  nmfnsetn0  31910  nmoplb  31939  nmfnlb  31956  lnopunilem1  32042  elunop2  32045  nmcexi  32058  lnconi  32065  branmfn  32137  pjbdlni  32181  pjss2coi  32196  pjdifnormi  32199  cdj3lem2b  32469  cdj3i  32473  fsumiunle  32833  mgcmntco  32967  dfmgc2  32969  ismntoplly  33971  prodindf  33987  esumiun  34058  sitgval  34297  signstf0  34545  hgt750lemg  34631  subfacp1lem4  35151  cvmliftlem3  35255  cvmliftlem15  35266  satfv0fvfmla0  35381  msubvrs  35528  sinccvg  35641  iprodefisumlem  35702  opnregcld  36296  cldregopn  36297  unblimceq0lem  36472  unbdqndv2  36477  bj-inftyexpitaudisj  37171  poimirlem5  37585  poimirlem6  37586  poimirlem7  37587  poimirlem8  37588  poimirlem10  37590  poimirlem11  37591  poimirlem12  37592  poimirlem13  37593  poimirlem14  37594  poimirlem15  37595  poimirlem16  37596  poimirlem17  37597  poimirlem18  37598  poimirlem19  37599  poimirlem20  37600  poimirlem21  37601  poimirlem22  37602  poimirlem27  37607  poimirlem32  37612  mblfinlem2  37618  ovoliunnfl  37622  ex-ovoliunnfl  37623  ftc1anclem6  37658  prdsbnd2  37755  lflnegcl  39031  oposlem  39138  pmapglb2N  39728  polatN  39888  ispsubclN  39894  ispsubcl2N  39904  cdlemg16zz  40617  cdlemg40  40674  tendotp  40718  dvhvscacbv  41055  dvhvscaval  41056  dochlkr  41342  dochkrshp  41343  dochkrshp4  41346  djhfval  41354  lpolsatN  41445  lpolpolsatN  41446  lclkrlem2e  41468  lcfrvalsnN  41498  lcfrlem27  41526  lcfrlem37  41536  lcfr  41542  mapdordlem1a  41591  mapdordlem1  41593  mapdrvallem3  41603  mapdrval  41604  mapd0  41622  hdmap1vallem  41754  hdmap1cbv  41759  hdmapfval  41784  hgmapfval  41843  hgmapvv  41883  aks6d1c1p5  42069  aks6d1c1  42073  aks6d1c5lem3  42094  deg1gprod  42097  aks6d1c6lem1  42127  aks6d1c7lem3  42139  ismrcd2  42655  ismrc  42657  hbt  43087  mpaaval  43108  cantnfub  43283  ntrclsk4  44034  dvgrat  44281  mccllem  45518  mccl  45519  climsuse  45529  limsupref  45606  climbddf  45608  dvbdfbdioolem2  45850  dvbdfbdioo  45851  ioodvbdlimc1lem1  45852  ioodvbdlimc1lem2  45853  ioodvbdlimc1  45854  ioodvbdlimc2lem  45855  ioodvbdlimc2  45856  stirlinglem4  45998  stirlinglem11  46005  stirlinglem12  46006  stirlinglem13  46007  stirlinglem14  46008  etransclem48  46203  ioorrnopn  46226  ioorrnopnxr  46228  voliunsge0lem  46393  meaiuninclem  46401  meaiuninc  46402  meaiunincf  46404  meaiuninc3v  46405  meaiuninc3  46406  meaiininc  46408  omeiunle  46438  omeiunltfirp  46440  caratheodorylem1  46447  vonval  46461  ovn0lem  46486  ovnsubaddlem1  46491  ovnsubaddlem2  46492  ovnsubadd  46493  hoidmvlelem5  46520  ovnhoilem2  46523  hoiqssbl  46546  hspmbllem2  46548  hspmbl  46550  opnvonmbllem2  46554  ovnsubadd2lem  46566  ovolval4lem2  46571  ovolval4  46572  ovolval5lem2  46574  ovolval5lem3  46575  ovnovollem1  46577  ovnovollem2  46578  vonioolem2  46602  vonicclem2  46605  fargshiftfva  47317  isuspgrim0lem  47755  isuspgrim0  47756  grimuhgr  47762  grimcnv  47763  grimco  47764  gricushgr  47770  uhgrimisgrgriclem  47782  clnbgrgrimlem  47785  clnbgrgrim  47786  grimedg  47787  uspgrlimlem3  47814  lincop  48137  lcoop  48140  ldepsnlinc  48237  lines  48465