Theorem 2fveq3 6884

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

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

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 2147  ax-9 2155  ax-ext 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541

This theorem is used by:  nvocnv  7283  2fvcoidd  7299  caofinvl  7711  oteqimp  8006  el2xptp0  8034  sbcoteq1a  8049  frpoins3xp3g  8140  xpord3lem  8148  seqomlem1  8440  xpmapen  9144  cnfcom  9680  updjudhcoinlf  9938  updjudhcoinrg  9939  acndom  10055  fodomacn  10060  alephcard  10074  iunfictbso  10118  ackbij2lem2  10242  axcc2  10440  axdc3lem2  10454  axdc3  10457  axdc4lem  10458  pwcfsdom  10593  pwfseqlem1  10668  pwfseqlem2  10669  rankcf  10787  recrecnq  10977  om2uzrdg  14021  uzrdgfni  14023  seqhomo  14114  hashf1  14523  seqcoll  14530  splval  14821  splcl  14822  o1co  15674  iseralt  15773  fsumf1o  15810  fsumrelem  15895  iserabs  15903  cvgcmpce  15906  supcvg  15946  explecnv  15955  cvgrat  15973  fprodf1o  16034  ruclem8  16326  ruclem9  16327  alginv  16666  algcvg  16667  algcvga  16670  iserodd  16928  prdsbasprj  17558  prdsplusgfval  17560  prdsmulrfval  17562  prdsvscafval  17566  prdsbas3  17567  prdsdsval2  17570  xpsle  17666  funcf2  17958  funcid  17960  funcpropd  17992  yonedalem3b  18368  yoniso  18374  prdsinvlem  19173  efgredlemd  19872  efgred  19876  dprdcntz  20138  ablfaclem3  20217  iscss  21897  prdsinvgd2  21956  evlslem1  22299  m1detdiag  22820  m2detleib  22854  cramerlem1  22913  pmatcoe1fsupp  22927  mat2pmatfval  22949  cpmadugsumlemF  23102  cpmadugsumfi  23103  cpmadumatpoly  23109  chcoeffeqlem  23111  cayhamlem3  23113  cayleyhamilton  23116  ptcld  23840  ptcldmpt  23841  dfac14  23845  alexsubALTlem1  24274  iscusp  24525  imasdsf1olem  24600  xpsdsval  24608  prdsxmslem2  24756  nmolb2d  24945  nmoi  24955  nmoleub2lem2  25345  nmoleub3  25348  caubl  25537  caublcls  25538  bcthlem4  25556  ovollb2lem  25717  ovollb2  25718  ovoliunlem1  25731  ovoliunlem2  25732  ovolshftlem2  25739  ovolscalem2  25743  ovolicc2lem1  25746  ovolicc2lem3  25748  ovolicc2lem4  25749  ovolicc2lem5  25750  ovolicc2  25751  voliunlem3  25781  voliun  25783  volsup  25785  ioombl1  25791  ovolfs2  25800  ioorinv  25805  uniioombllem2  25812  uniioombllem3  25814  uniioombllem4  25815  uniioombllem6  25817  dyadmbl  25829  mbflim  25897  itg2seq  25971  itg2monolem1  25979  itg2monolem2  25980  itg2monolem3  25981  itg2mono  25982  itg2i1fseq2  25985  itg2addlem  25987  bddmulibl  26067  bddiblnc  26070  dvlipcn  26222  c1liplem1  26224  dvfsumabs  26251  ftc1a  26265  aannenlem2  26566  aalioulem4  26572  radcnvlem2  26651  radcnvlt2  26656  dvradcnv  26658  pserulm  26659  abelthlem5  26672  abelthlem8  26676  logcnlem5  26884  lgamgulmlem2  27267  lgamgulmlem6  27271  ftalem2  27311  ftalem3  27312  ftalem5  27314  ftalem7  27316  fta  27317  bposlem7  27527  bposlem9  27529  rpvmasumlem  27724  dchrisumlem1  27726  dchrisumlem2  27727  dchrisumlem3  27728  dchrisum  27729  dchrmusumlema  27730  dchrmusum2  27731  dchrvmasumlem1  27732  dchrvmasum2lem  27733  dchrvmasumlema  27737  dchrvmasumiflem1  27738  dchrvmaeq0  27741  dchrisum0fval  27742  dchrisum0fmul  27743  dchrisum0ff  27744  dchrisum0flblem1  27745  dchrisum0re  27750  dchrisum0lema  27751  dchrisum0lem1b  27752  dchrisum0lem2a  27754  dchrisum0lem2  27755  rpvmasum  27763  pntlemo  27844  leftval  28115  rightval  28116  addsval  28228  negbdaylem  28322  om2noseqrdg  28570  expsval  28691  ewlkinedg  30065  wkslem1  30068  wkslem2  30069  2wlklem  30126  wlkdlem2  30142  upgrwlkdvdelem  30202  crctcshwlkn0lem4  30282  crctcshwlkn0lem5  30283  wlksnwwlknvbij  30377  2wlkdlem10  30404  clwlkclwwlklem1  30470  clwlkclwwlklem2  30471  clwlkclwwlkfolem  30478  clwlkclwwlkfo  30480  clwlkclwwlkf1  30481  clwlkclwwlken  30483  clwlknf1oclwwlknlem2  30553  clwlknf1oclwwlkn  30555  3wlkdlem10  30650  eupthseg  30687  upgreupthseg  30690  eupth2lem3  30717  fusgreghash2wsp  30819  clwwlknonclwlknonf1o  30843  dlwwlknondlwlknonf1o  30846  nmosetn0  31247  nmoolb  31253  nmounbseqi  31259  nmobndseqi  31261  nmlno0lem  31275  nmlnoubi  31278  blocnilem  31286  ubthlem1  31352  ubthlem2  31353  ubthlem3  31354  ococ  31888  pjoc1  31916  chscllem2  32120  chscllem3  32121  pjinormi  32169  pjnorm  32206  pjpyth  32207  pjnel  32208  nmopsetn0  32347  nmfnsetn0  32360  nmoplb  32389  nmfnlb  32406  lnopunilem1  32492  elunop2  32495  nmcexi  32508  lnconi  32515  branmfn  32587  pjbdlni  32631  pjss2coi  32646  pjdifnormi  32649  cdj3lem2b  32919  cdj3i  32923  fsumiunle  33300  prodindf  33309  mgcmntco  33435  dfmgc2  33437  elrgspnsubrunlem2  33689  deg1prod  33994  psrmonprod  34063  vietadeg1  34089  vietalem  34090  vieta  34091  ismntoplly  34536  esumiun  34605  sitgval  34844  signstf0  35077  hgt750lemg  35163  onvf1odlem4  35704  subfacp1lem4  35763  cvmliftlem3  35867  cvmliftlem15  35878  satfv0fvfmla0  35993  msubvrs  36140  sinccvg  36253  iprodefisumlem  36320  opnregcld  36950  cldregopn  36951  unblimceq0lem  37204  unbdqndv2  37209  bj-inftyexpitaudisj  37958  poimirlem5  38375  poimirlem6  38376  poimirlem7  38377  poimirlem8  38378  poimirlem10  38380  poimirlem11  38381  poimirlem12  38382  poimirlem13  38383  poimirlem14  38384  poimirlem15  38385  poimirlem16  38386  poimirlem17  38387  poimirlem18  38388  poimirlem19  38389  poimirlem20  38390  poimirlem21  38391  poimirlem22  38392  poimirlem27  38397  poimirlem32  38402  mblfinlem2  38408  ovoliunnfl  38412  ex-ovoliunnfl  38413  ftc1anclem6  38448  prdsbnd2  38546  lflnegcl  39949  oposlem  40056  pmapglb2N  40645  polatN  40805  ispsubclN  40811  ispsubcl2N  40821  cdlemg16zz  41534  cdlemg40  41591  tendotp  41635  dvhvscacbv  41972  dvhvscaval  41973  dochlkr  42259  dochkrshp  42260  dochkrshp4  42263  djhfval  42271  lpolsatN  42362  lpolpolsatN  42363  lclkrlem2e  42385  lcfrvalsnN  42415  lcfrlem27  42443  lcfrlem37  42453  lcfr  42459  mapdordlem1a  42508  mapdordlem1  42510  mapdrvallem3  42520  mapdrval  42521  mapd0  42539  hdmap1vallem  42671  hdmap1cbv  42676  hdmapfval  42701  hgmapfval  42760  hgmapvv  42800  aks6d1c1p5  42979  aks6d1c1  42983  aks6d1c5lem3  43004  deg1gprod  43007  aks6d1c6lem1  43037  aks6d1c7lem3  43049  readvcot  43240  ismrcd2  43545  ismrc  43547  hbt  43972  mpaaval  43993  cantnfub  44163  ntrclsk4  44913  dvgrat  45137  mccllem  46428  mccl  46429  climsuse  46439  limsupref  46514  climbddf  46516  dvbdfbdioolem2  46758  dvbdfbdioo  46759  ioodvbdlimc1lem1  46760  ioodvbdlimc1lem2  46761  ioodvbdlimc1  46762  ioodvbdlimc2lem  46763  ioodvbdlimc2  46764  stirlinglem4  46906  stirlinglem11  46913  stirlinglem12  46914  stirlinglem13  46915  stirlinglem14  46916  etransclem48  47111  ioorrnopn  47134  ioorrnopnxr  47136  voliunsge0lem  47301  meaiuninclem  47309  meaiuninc  47310  meaiunincf  47312  meaiuninc3v  47313  meaiuninc3  47314  meaiininc  47316  omeiunle  47346  omeiunltfirp  47348  caratheodorylem1  47355  vonval  47369  ovn0lem  47394  ovnsubaddlem1  47399  ovnsubaddlem2  47400  ovnsubadd  47401  hoidmvlelem5  47428  ovnhoilem2  47431  hoiqssbl  47454  hspmbllem2  47456  hspmbl  47458  opnvonmbllem2  47462  ovnsubadd2lem  47474  ovolval4lem2  47479  ovolval4  47480  ovolval5lem2  47482  ovolval5lem3  47483  ovnovollem1  47485  ovnovollem2  47486  vonioolem2  47510  vonicclem2  47513  fargshiftfva  48344  grimuhgr  48804  grimcnv  48805  grimco  48806  uhgrimedgi  48807  isuspgrim0lem  48810  isuspgrim0  48811  upgrimwlklem3  48816  upgrimwlklem5  48818  upgrimtrls  48823  gricushgr  48834  cycldlenngric  48845  uhgrimisgrgriclem  48847  clnbgrgrimlem  48850  clnbgrgrim  48851  grimedg  48852  uspgrlimlem3  48907  lincop  49339  lcoop  49342  ldepsnlinc  49439  lines  49662  oppcinito  50162  oppctermo  50163  fucoid  50275  veronesematbasd  50814  veronesematrowd  50815  veronesematrowexpd  50816  veroquadmodzerod  50818  veroquadnolindfd  50819  veroquaddetzerod  50820