Theorem 2fveq3 6921

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574

This theorem is used by:  nvocnv  7320  2fvcoidd  7336  caofinvl  7757  oteqimp  8054  el2xptp0  8081  sbcoteq1a  8097  frpoins3xp3g  8195  xpord3lem  8203  seqomlem1  8498  xpmapen  9202  cnfcom  9738  updjudhcoinlf  10050  updjudhcoinrg  10051  acndom  10169  fodomacn  10174  alephcard  10188  iunfictbso  10232  ackbij2lem2  10356  axcc2  10554  axdc3lem2  10568  axdc3  10571  axdc4lem  10572  pwcfsdom  10707  pwfseqlem1  10782  pwfseqlem2  10783  rankcf  10901  recrecnq  11091  om2uzrdg  14139  uzrdgfni  14141  seqhomo  14232  hashf1  14643  seqcoll  14650  splval  14942  splcl  14943  o1co  15797  iseralt  15896  fsumf1o  15933  fsumrelem  16018  iserabs  16026  cvgcmpce  16029  supcvg  16069  explecnv  16078  cvgrat  16096  fprodf1o  16157  ruclem8  16449  ruclem9  16450  alginv  16794  algcvg  16795  algcvga  16798  iserodd  17057  prdsbasprj  17693  prdsplusgfval  17695  prdsmulrfval  17697  prdsvscafval  17701  prdsbas3  17702  prdsdsval2  17705  xpsle  17801  funcf2  18093  funcid  18095  funcpropd  18127  yonedalem3b  18503  yoniso  18509  prdsinvlem  19309  efgredlemd  20009  efgred  20013  dprdcntz  20275  ablfaclem3  20354  iscss  22044  prdsinvgd2  22103  evlslem1  22446  m1detdiag  22967  m2detleib  23001  cramerlem1  23060  pmatcoe1fsupp  23074  mat2pmatfval  23096  cpmadugsumlemF  23249  cpmadugsumfi  23250  cpmadumatpoly  23256  chcoeffeqlem  23258  cayhamlem3  23260  cayleyhamilton  23263  ptcld  23987  ptcldmpt  23988  dfac14  23992  alexsubALTlem1  24421  iscusp  24672  imasdsf1olem  24747  xpsdsval  24755  prdsxmslem2  24903  nmolb2d  25092  nmoi  25102  nmoleub2lem2  25492  nmoleub3  25495  caubl  25684  caublcls  25685  bcthlem4  25703  ovollb2lem  25864  ovollb2  25865  ovoliunlem1  25878  ovoliunlem2  25879  ovolshftlem2  25886  ovolscalem2  25890  ovolicc2lem1  25893  ovolicc2lem3  25895  ovolicc2lem4  25896  ovolicc2lem5  25897  ovolicc2  25898  voliunlem3  25928  voliun  25930  volsup  25932  ioombl1  25938  ovolfs2  25947  ioorinv  25952  uniioombllem2  25959  uniioombllem3  25961  uniioombllem4  25962  uniioombllem6  25964  dyadmbl  25976  mbflim  26044  itg2seq  26118  itg2monolem1  26126  itg2monolem2  26127  itg2monolem3  26128  itg2mono  26129  itg2i1fseq2  26132  itg2addlem  26134  bddmulibl  26214  bddiblnc  26217  dvlipcn  26369  c1liplem1  26371  dvfsumabs  26398  ftc1a  26412  aannenlem2  26713  aalioulem4  26719  radcnvlem2  26798  radcnvlt2  26803  dvradcnv  26805  pserulm  26806  abelthlem5  26819  abelthlem8  26823  logcnlem5  27031  lgamgulmlem2  27414  lgamgulmlem6  27418  ftalem2  27458  ftalem3  27459  ftalem5  27461  ftalem7  27463  fta  27464  bposlem7  27674  bposlem9  27676  rpvmasumlem  27871  dchrisumlem1  27873  dchrisumlem2  27874  dchrisumlem3  27875  dchrisum  27876  dchrmusumlema  27877  dchrmusum2  27878  dchrvmasumlem1  27879  dchrvmasum2lem  27880  dchrvmasumlema  27884  dchrvmasumiflem1  27885  dchrvmaeq0  27888  dchrisum0fval  27889  dchrisum0fmul  27890  dchrisum0ff  27891  dchrisum0flblem1  27892  dchrisum0re  27897  dchrisum0lema  27898  dchrisum0lem1b  27899  dchrisum0lem2a  27901  dchrisum0lem2  27902  rpvmasum  27910  pntlemo  27991  leftval  28292  rightval  28293  addsval  28405  negbdaylem  28499  om2noseqrdg  28747  expsval  28868  ewlkinedg  30242  wkslem1  30245  wkslem2  30246  2wlklem  30303  wlkdlem2  30319  upgrwlkdvdelem  30379  crctcshwlkn0lem4  30459  crctcshwlkn0lem5  30460  wlksnwwlknvbij  30554  2wlkdlem10  30581  clwlkclwwlklem1  30647  clwlkclwwlklem2  30648  clwlkclwwlkfolem  30655  clwlkclwwlkfo  30657  clwlkclwwlkf1  30658  clwlkclwwlken  30660  clwlknf1oclwwlknlem2  30730  clwlknf1oclwwlkn  30732  3wlkdlem10  30827  eupthseg  30864  upgreupthseg  30867  eupth2lem3  30894  fusgreghash2wsp  30996  clwwlknonclwlknonf1o  31020  dlwwlknondlwlknonf1o  31023  nmosetn0  31424  nmoolb  31430  nmounbseqi  31436  nmobndseqi  31438  nmlno0lem  31452  nmlnoubi  31455  blocnilem  31463  ubthlem1  31529  ubthlem2  31530  ubthlem3  31531  ococ  32065  pjoc1  32093  chscllem2  32297  chscllem3  32298  pjinormi  32346  pjnorm  32383  pjpyth  32384  pjnel  32385  nmopsetn0  32524  nmfnsetn0  32537  nmoplb  32566  nmfnlb  32583  lnopunilem1  32669  elunop2  32672  nmcexi  32685  lnconi  32692  branmfn  32764  pjbdlni  32808  pjss2coi  32823  pjdifnormi  32826  cdj3lem2b  33096  cdj3i  33100  fsumiunle  33516  prodindf  33525  mgcmntco  33654  dfmgc2  33656  elrgspnsubrunlem2  33908  deg1prod  34218  psrmonprod  34295  vietadeg1  34321  vietalem  34322  vieta  34323  ismntoplly  34768  esumiun  34837  sitgval  35075  signstf0  35308  hgt750lemg  35394  jf1  36051  k1on  36056  k2on  36057  k39o  36058  jk1k2k3  36059  onvf1odlem4  36075  subfacp1lem4  36156  cvmliftlem3  36260  cvmliftlem15  36271  satfv0fvfmla0  36386  msubvrs  36533  sinccvg  36646  iprodefisumlem  36720  opnregcld  37333  cldregopn  37334  unblimceq0lem  37587  unbdqndv2  37592  bj-inftyexpitaudisj  38394  poimirlem5  38811  poimirlem6  38812  poimirlem7  38813  poimirlem8  38814  poimirlem10  38816  poimirlem11  38817  poimirlem12  38818  poimirlem13  38819  poimirlem14  38820  poimirlem15  38821  poimirlem16  38822  poimirlem17  38823  poimirlem18  38824  poimirlem19  38825  poimirlem20  38826  poimirlem21  38827  poimirlem22  38828  poimirlem27  38833  poimirlem32  38838  mblfinlem2  38844  ovoliunnfl  38848  ex-ovoliunnfl  38849  ftc1anclem6  38884  prdsbnd2  38995  lflnegcl  40398  oposlem  40505  pmapglb2N  41094  polatN  41254  ispsubclN  41260  ispsubcl2N  41270  cdlemg16zz  41983  cdlemg40  42040  tendotp  42084  dvhvscacbv  42421  dvhvscaval  42422  dochlkr  42708  dochkrshp  42709  dochkrshp4  42712  djhfval  42720  lpolsatN  42811  lpolpolsatN  42812  lclkrlem2e  42834  lcfrvalsnN  42864  lcfrlem27  42892  lcfrlem37  42902  lcfr  42908  mapdordlem1a  42957  mapdordlem1  42959  mapdrvallem3  42969  mapdrval  42970  mapd0  42988  hdmap1vallem  43120  hdmap1cbv  43125  hdmapfval  43150  hgmapfval  43209  hgmapvv  43249  aks6d1c1p5  43428  aks6d1c1  43432  aks6d1c5lem3  43453  deg1gprod  43456  aks6d1c6lem1  43486  aks6d1c7lem3  43498  readvcot  43681  ismrcd2  43976  ismrc  43978  hbt  44397  mpaaval  44418  cantnfub  44584  ntrclsk4  45333  dvgrat  45557  mccllem  46882  mccl  46883  climsuse  46893  limsupref  46968  climbddf  46970  dvbdfbdioolem2  47212  dvbdfbdioo  47213  ioodvbdlimc1lem1  47214  ioodvbdlimc1lem2  47215  ioodvbdlimc1  47216  ioodvbdlimc2lem  47217  ioodvbdlimc2  47218  stirlinglem4  47360  stirlinglem11  47367  stirlinglem12  47368  stirlinglem13  47369  stirlinglem14  47370  etransclem48  47565  ioorrnopn  47588  ioorrnopnxr  47590  voliunsge0lem  47755  meaiuninclem  47763  meaiuninc  47764  meaiunincf  47766  meaiuninc3v  47767  meaiuninc3  47768  meaiininc  47770  omeiunle  47800  omeiunltfirp  47802  caratheodorylem1  47809  vonval  47823  ovn0lem  47848  ovnsubaddlem1  47853  ovnsubaddlem2  47854  ovnsubadd  47855  hoidmvlelem5  47882  ovnhoilem2  47885  hoiqssbl  47908  hspmbllem2  47910  hspmbl  47912  opnvonmbllem2  47916  ovnsubadd2lem  47928  ovolval4lem2  47933  ovolval4  47934  ovolval5lem2  47936  ovolval5lem3  47937  ovnovollem1  47939  ovnovollem2  47940  vonioolem2  47964  vonicclem2  47967  fargshiftfva  48798  grimuhgr  49258  grimcnv  49259  grimco  49260  uhgrimedgi  49261  isuspgrim0lem  49264  isuspgrim0  49265  upgrimwlklem3  49270  upgrimwlklem5  49272  upgrimtrls  49277  gricushgr  49288  cycldlenngric  49299  uhgrimisgrgriclem  49301  clnbgrgrimlem  49304  clnbgrgrim  49305  grimedg  49306  uspgrlimlem3  49361  lincop  49851  lcoop  49854  ldepsnlinc  49951  lines  50175  ixpovf  50528  oppcinito  50688  oppctermo  50689  fucoid  50801  veronesematbasd  51408  veronesematrowd  51409  veronesematrowexpd  51410  veroquadmodzerod  51412  veroquadnolindfd  51413  veroquaddetzerod  51414