Theorem 2fveq3 6543

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

Syntax hints:   → wi 4   = wceq 1522  ‘cfv 6225

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-rex 3111  df-rab 3114  df-v 3439  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-br 4963  df-iota 6189  df-fv 6233

This theorem is referenced by:  nvocnv  6903  2fvcoidd  6918  caofinvl  7294  oteqimp  7564  el2xptp0  7592  seqomlem1  7937  xpmapen  8532  cnfcom  9009  updjudhcoinlf  9207  updjudhcoinrg  9208  acndom  9323  fodomacn  9328  alephcard  9342  iunfictbso  9386  ackbij2lem2  9508  axcc2  9705  axdc3lem2  9719  axdc3  9722  axdc4lem  9723  pwcfsdom  9851  pwfseqlem1  9926  pwfseqlem2  9927  rankcf  10045  recrecnq  10235  om2uzrdg  13174  uzrdgfni  13176  seqhomo  13267  hashf1  13663  seqcoll  13670  splval  13949  splcl  13950  o1co  14777  iseralt  14875  fsumf1o  14913  fsumrelem  14995  iserabs  15003  cvgcmpce  15006  supcvg  15044  explecnv  15053  cvgrat  15072  fprodf1o  15133  ruclem8  15423  ruclem9  15424  alginv  15748  algcvg  15749  algcvga  15752  iserodd  16001  prdsbasprj  16574  prdsplusgfval  16576  prdsmulrfval  16578  prdsvscafval  16582  prdsbas3  16583  prdsdsval2  16586  xpsle  16681  funcf2  16967  funcid  16969  funcpropd  16999  yonedalem3b  17358  yoniso  17364  prdsinvlem  17965  efgredlemd  18597  efgred  18601  dprdcntz  18847  ablfaclem3  18926  evlslem1  19982  iscss  20509  prdsinvgd2  20568  m1detdiag  20890  m2detleib  20924  cramerlem1  20980  pmatcoe1fsupp  20993  mat2pmatfval  21015  cpmadugsumlemF  21168  cpmadugsumfi  21169  cpmadumatpoly  21175  chcoeffeqlem  21177  cayhamlem3  21179  cayleyhamilton  21182  ptcld  21905  ptcldmpt  21906  dfac14  21910  alexsubALTlem1  22339  iscusp  22591  imasdsf1olem  22666  xpsdsval  22674  prdsxmslem2  22822  nmolb2d  23010  nmoi  23020  nmoleub2lem2  23403  nmoleub3  23406  caubl  23594  caublcls  23595  bcthlem4  23613  ovollb2lem  23772  ovollb2  23773  ovoliunlem1  23786  ovoliunlem2  23787  ovolshftlem2  23794  ovolscalem2  23798  ovolicc2lem1  23801  ovolicc2lem3  23803  ovolicc2lem4  23804  ovolicc2lem5  23805  ovolicc2  23806  voliunlem3  23836  voliun  23838  volsup  23840  ioombl1  23846  ovolfs2  23855  ioorinv  23860  uniioombllem2  23867  uniioombllem3  23869  uniioombllem4  23870  uniioombllem6  23872  dyadmbl  23884  mbflim  23952  itg2seq  24026  itg2monolem1  24034  itg2monolem2  24035  itg2monolem3  24036  itg2mono  24037  itg2i1fseq2  24040  itg2addlem  24042  bddmulibl  24122  dvlipcn  24274  c1liplem1  24276  dvfsumabs  24303  ftc1a  24317  aannenlem2  24601  aalioulem4  24607  radcnvlem2  24685  radcnvlt2  24690  dvradcnv  24692  pserulm  24693  abelthlem5  24706  abelthlem8  24710  logcnlem5  24910  lgamgulmlem2  25289  lgamgulmlem6  25293  ftalem2  25333  ftalem3  25334  ftalem5  25336  ftalem7  25338  fta  25339  bposlem7  25548  bposlem9  25550  rpvmasumlem  25745  dchrisumlem1  25747  dchrisumlem2  25748  dchrisumlem3  25749  dchrisum  25750  dchrmusumlema  25751  dchrmusum2  25752  dchrvmasumlem1  25753  dchrvmasum2lem  25754  dchrvmasumlema  25758  dchrvmasumiflem1  25759  dchrvmaeq0  25762  dchrisum0fval  25763  dchrisum0fmul  25764  dchrisum0ff  25765  dchrisum0flblem1  25766  dchrisum0re  25771  dchrisum0lema  25772  dchrisum0lem1b  25773  dchrisum0lem2a  25775  dchrisum0lem2  25776  rpvmasum  25784  pntlemo  25865  ewlkinedg  27069  wkslem1  27072  wkslem2  27073  2wlklem  27131  wlkdlem2  27150  upgrwlkdvdelem  27204  crctcshwlkn0lem4  27278  crctcshwlkn0lem5  27279  wlksnwwlknvbij  27374  2wlkdlem10  27401  clwlkclwwlklem1  27464  clwlkclwwlklem2  27465  clwlkclwwlkfolem  27472  clwlkclwwlkfo  27474  clwlkclwwlkf1  27475  clwlkclwwlken  27477  clwlknf1oclwwlknlem2  27548  clwlknf1oclwwlkn  27550  3wlkdlem10  27635  eupthseg  27672  upgreupthseg  27675  eupth2lem3  27703  fusgreghash2wsp  27809  clwwlknonclwlknonf1o  27833  dlwwlknondlwlknonf1o  27836  nmosetn0  28233  nmoolb  28239  nmounbseqi  28245  nmobndseqi  28247  nmlno0lem  28261  nmlnoubi  28264  blocnilem  28272  ubthlem1  28338  ubthlem2  28339  ubthlem3  28340  ococ  28874  pjoc1  28902  chscllem2  29106  chscllem3  29107  pjinormi  29155  pjnorm  29192  pjpyth  29193  pjnel  29194  nmopsetn0  29333  nmfnsetn0  29346  nmoplb  29375  nmfnlb  29392  lnopunilem1  29478  elunop2  29481  nmcexi  29494  lnconi  29501  branmfn  29573  pjbdlni  29617  pjss2coi  29632  pjdifnormi  29635  cdj3lem2b  29905  cdj3i  29909  fsumiunle  30229  ismntoplly  30883  prodindf  30899  esumiun  30970  sitgval  31207  signstf0  31455  hgt750lemg  31542  subfacp1lem4  32038  cvmliftlem3  32142  cvmliftlem15  32153  satfv0fvfmla0  32268  msubvrs  32415  sinccvg  32524  iprodefisumlem  32580  opnregcld  33287  cldregopn  33288  unblimceq0lem  33454  unbdqndv2  33459  bj-inftyexpitaudisj  34045  poimirlem5  34428  poimirlem6  34429  poimirlem7  34430  poimirlem8  34431  poimirlem10  34433  poimirlem11  34434  poimirlem12  34435  poimirlem13  34436  poimirlem14  34437  poimirlem15  34438  poimirlem16  34439  poimirlem17  34440  poimirlem18  34441  poimirlem19  34442  poimirlem20  34443  poimirlem21  34444  poimirlem22  34445  poimirlem27  34450  poimirlem32  34455  mblfinlem2  34461  ovoliunnfl  34465  ex-ovoliunnfl  34466  bddiblnc  34493  ftc1anclem6  34503  prdsbnd2  34605  lflnegcl  35742  oposlem  35849  pmapglb2N  36438  polatN  36598  ispsubclN  36604  ispsubcl2N  36614  cdlemg16zz  37327  cdlemg40  37384  tendotp  37428  dvhvscacbv  37765  dvhvscaval  37766  dochlkr  38052  dochkrshp  38053  dochkrshp4  38056  djhfval  38064  lpolsatN  38155  lpolpolsatN  38156  lclkrlem2e  38178  lcfrvalsnN  38208  lcfrlem27  38236  lcfrlem37  38246  lcfr  38252  mapdordlem1a  38301  mapdordlem1  38303  mapdrvallem3  38313  mapdrval  38314  mapd0  38332  hdmap1vallem  38464  hdmap1cbv  38469  hdmapfval  38494  hgmapfval  38553  hgmapvv  38593  ismrcd2  38781  ismrc  38783  hbt  39215  mpaaval  39236  ntrclsk4  39907  dvgrat  40182  mccllem  41420  mccl  41421  climsuse  41431  limsupref  41508  climbddf  41510  dvbdfbdioolem2  41755  dvbdfbdioo  41756  ioodvbdlimc1lem1  41757  ioodvbdlimc1lem2  41758  ioodvbdlimc1  41759  ioodvbdlimc2lem  41760  ioodvbdlimc2  41761  stirlinglem4  41904  stirlinglem11  41911  stirlinglem12  41912  stirlinglem13  41913  stirlinglem14  41914  etransclem48  42109  ioorrnopn  42132  ioorrnopnxr  42134  voliunsge0lem  42296  meaiuninclem  42304  meaiuninc  42305  meaiunincf  42307  meaiuninc3v  42308  meaiuninc3  42309  meaiininc  42311  omeiunle  42341  omeiunltfirp  42343  caratheodorylem1  42350  vonval  42364  ovn0lem  42389  ovnsubaddlem1  42394  ovnsubaddlem2  42395  ovnsubadd  42396  hoidmvlelem5  42423  ovnhoilem2  42426  hoiqssbl  42449  hspmbllem2  42451  hspmbl  42453  opnvonmbllem2  42457  ovnsubadd2lem  42469  ovolval4lem2  42474  ovolval4  42475  ovolval5lem2  42477  ovolval5lem3  42478  ovnovollem1  42480  ovnovollem2  42481  vonioolem2  42505  vonicclem2  42508  fargshiftfva  43085  isomushgr  43473  isomgrsym  43483  isomgrtrlem  43485  lincop  43943  lcoop  43946  ldepsnlinc  44043  lines  44199