Theorem 2fveq3 6675

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363

This theorem is referenced by:  nvocnv  7038  2fvcoidd  7053  caofinvl  7436  oteqimp  7708  el2xptp0  7736  seqomlem1  8086  xpmapen  8685  cnfcom  9163  updjudhcoinlf  9361  updjudhcoinrg  9362  acndom  9477  fodomacn  9482  alephcard  9496  iunfictbso  9540  ackbij2lem2  9662  axcc2  9859  axdc3lem2  9873  axdc3  9876  axdc4lem  9877  pwcfsdom  10005  pwfseqlem1  10080  pwfseqlem2  10081  rankcf  10199  recrecnq  10389  om2uzrdg  13325  uzrdgfni  13327  seqhomo  13418  hashf1  13816  seqcoll  13823  splval  14113  splcl  14114  o1co  14943  iseralt  15041  fsumf1o  15080  fsumrelem  15162  iserabs  15170  cvgcmpce  15173  supcvg  15211  explecnv  15220  cvgrat  15239  fprodf1o  15300  ruclem8  15590  ruclem9  15591  alginv  15919  algcvg  15920  algcvga  15923  iserodd  16172  prdsbasprj  16745  prdsplusgfval  16747  prdsmulrfval  16749  prdsvscafval  16753  prdsbas3  16754  prdsdsval2  16757  xpsle  16852  funcf2  17138  funcid  17140  funcpropd  17170  yonedalem3b  17529  yoniso  17535  prdsinvlem  18208  efgredlemd  18870  efgred  18874  dprdcntz  19130  ablfaclem3  19209  evlslem1  20295  iscss  20827  prdsinvgd2  20886  m1detdiag  21206  m2detleib  21240  cramerlem1  21296  pmatcoe1fsupp  21309  mat2pmatfval  21331  cpmadugsumlemF  21484  cpmadugsumfi  21485  cpmadumatpoly  21491  chcoeffeqlem  21493  cayhamlem3  21495  cayleyhamilton  21498  ptcld  22221  ptcldmpt  22222  dfac14  22226  alexsubALTlem1  22655  iscusp  22908  imasdsf1olem  22983  xpsdsval  22991  prdsxmslem2  23139  nmolb2d  23327  nmoi  23337  nmoleub2lem2  23720  nmoleub3  23723  caubl  23911  caublcls  23912  bcthlem4  23930  ovollb2lem  24089  ovollb2  24090  ovoliunlem1  24103  ovoliunlem2  24104  ovolshftlem2  24111  ovolscalem2  24115  ovolicc2lem1  24118  ovolicc2lem3  24120  ovolicc2lem4  24121  ovolicc2lem5  24122  ovolicc2  24123  voliunlem3  24153  voliun  24155  volsup  24157  ioombl1  24163  ovolfs2  24172  ioorinv  24177  uniioombllem2  24184  uniioombllem3  24186  uniioombllem4  24187  uniioombllem6  24189  dyadmbl  24201  mbflim  24269  itg2seq  24343  itg2monolem1  24351  itg2monolem2  24352  itg2monolem3  24353  itg2mono  24354  itg2i1fseq2  24357  itg2addlem  24359  bddmulibl  24439  dvlipcn  24591  c1liplem1  24593  dvfsumabs  24620  ftc1a  24634  aannenlem2  24918  aalioulem4  24924  radcnvlem2  25002  radcnvlt2  25007  dvradcnv  25009  pserulm  25010  abelthlem5  25023  abelthlem8  25027  logcnlem5  25229  lgamgulmlem2  25607  lgamgulmlem6  25611  ftalem2  25651  ftalem3  25652  ftalem5  25654  ftalem7  25656  fta  25657  bposlem7  25866  bposlem9  25868  rpvmasumlem  26063  dchrisumlem1  26065  dchrisumlem2  26066  dchrisumlem3  26067  dchrisum  26068  dchrmusumlema  26069  dchrmusum2  26070  dchrvmasumlem1  26071  dchrvmasum2lem  26072  dchrvmasumlema  26076  dchrvmasumiflem1  26077  dchrvmaeq0  26080  dchrisum0fval  26081  dchrisum0fmul  26082  dchrisum0ff  26083  dchrisum0flblem1  26084  dchrisum0re  26089  dchrisum0lema  26090  dchrisum0lem1b  26091  dchrisum0lem2a  26093  dchrisum0lem2  26094  rpvmasum  26102  pntlemo  26183  ewlkinedg  27386  wkslem1  27389  wkslem2  27390  2wlklem  27449  wlkdlem2  27465  upgrwlkdvdelem  27517  crctcshwlkn0lem4  27591  crctcshwlkn0lem5  27592  wlksnwwlknvbij  27687  2wlkdlem10  27714  clwlkclwwlklem1  27777  clwlkclwwlklem2  27778  clwlkclwwlkfolem  27785  clwlkclwwlkfo  27787  clwlkclwwlkf1  27788  clwlkclwwlken  27790  clwlknf1oclwwlknlem2  27861  clwlknf1oclwwlkn  27863  3wlkdlem10  27948  eupthseg  27985  upgreupthseg  27988  eupth2lem3  28015  fusgreghash2wsp  28117  clwwlknonclwlknonf1o  28141  dlwwlknondlwlknonf1o  28144  nmosetn0  28542  nmoolb  28548  nmounbseqi  28554  nmobndseqi  28556  nmlno0lem  28570  nmlnoubi  28573  blocnilem  28581  ubthlem1  28647  ubthlem2  28648  ubthlem3  28649  ococ  29183  pjoc1  29211  chscllem2  29415  chscllem3  29416  pjinormi  29464  pjnorm  29501  pjpyth  29502  pjnel  29503  nmopsetn0  29642  nmfnsetn0  29655  nmoplb  29684  nmfnlb  29701  lnopunilem1  29787  elunop2  29790  nmcexi  29803  lnconi  29810  branmfn  29882  pjbdlni  29926  pjss2coi  29941  pjdifnormi  29944  cdj3lem2b  30214  cdj3i  30218  fsumiunle  30545  ismntoplly  31266  prodindf  31282  esumiun  31353  sitgval  31590  signstf0  31838  hgt750lemg  31925  subfacp1lem4  32430  cvmliftlem3  32534  cvmliftlem15  32545  satfv0fvfmla0  32660  msubvrs  32807  sinccvg  32916  iprodefisumlem  32972  opnregcld  33678  cldregopn  33679  unblimceq0lem  33845  unbdqndv2  33850  bj-inftyexpitaudisj  34490  poimirlem5  34912  poimirlem6  34913  poimirlem7  34914  poimirlem8  34915  poimirlem10  34917  poimirlem11  34918  poimirlem12  34919  poimirlem13  34920  poimirlem14  34921  poimirlem15  34922  poimirlem16  34923  poimirlem17  34924  poimirlem18  34925  poimirlem19  34926  poimirlem20  34927  poimirlem21  34928  poimirlem22  34929  poimirlem27  34934  poimirlem32  34939  mblfinlem2  34945  ovoliunnfl  34949  ex-ovoliunnfl  34950  bddiblnc  34977  ftc1anclem6  34987  prdsbnd2  35088  lflnegcl  36226  oposlem  36333  pmapglb2N  36922  polatN  37082  ispsubclN  37088  ispsubcl2N  37098  cdlemg16zz  37811  cdlemg40  37868  tendotp  37912  dvhvscacbv  38249  dvhvscaval  38250  dochlkr  38536  dochkrshp  38537  dochkrshp4  38540  djhfval  38548  lpolsatN  38639  lpolpolsatN  38640  lclkrlem2e  38662  lcfrvalsnN  38692  lcfrlem27  38720  lcfrlem37  38730  lcfr  38736  mapdordlem1a  38785  mapdordlem1  38787  mapdrvallem3  38797  mapdrval  38798  mapd0  38816  hdmap1vallem  38948  hdmap1cbv  38953  hdmapfval  38978  hgmapfval  39037  hgmapvv  39077  ismrcd2  39345  ismrc  39347  hbt  39779  mpaaval  39800  ntrclsk4  40471  dvgrat  40693  mccllem  41927  mccl  41928  climsuse  41938  limsupref  42015  climbddf  42017  dvbdfbdioolem2  42263  dvbdfbdioo  42264  ioodvbdlimc1lem1  42265  ioodvbdlimc1lem2  42266  ioodvbdlimc1  42267  ioodvbdlimc2lem  42268  ioodvbdlimc2  42269  stirlinglem4  42411  stirlinglem11  42418  stirlinglem12  42419  stirlinglem13  42420  stirlinglem14  42421  etransclem48  42616  ioorrnopn  42639  ioorrnopnxr  42641  voliunsge0lem  42803  meaiuninclem  42811  meaiuninc  42812  meaiunincf  42814  meaiuninc3v  42815  meaiuninc3  42816  meaiininc  42818  omeiunle  42848  omeiunltfirp  42850  caratheodorylem1  42857  vonval  42871  ovn0lem  42896  ovnsubaddlem1  42901  ovnsubaddlem2  42902  ovnsubadd  42903  hoidmvlelem5  42930  ovnhoilem2  42933  hoiqssbl  42956  hspmbllem2  42958  hspmbl  42960  opnvonmbllem2  42964  ovnsubadd2lem  42976  ovolval4lem2  42981  ovolval4  42982  ovolval5lem2  42984  ovolval5lem3  42985  ovnovollem1  42987  ovnovollem2  42988  vonioolem2  43012  vonicclem2  43015  fargshiftfva  43652  isomushgr  44040  isomgrsym  44050  isomgrtrlem  44052  lincop  44512  lcoop  44515  ldepsnlinc  44612  lines  44767