Theorem fvoveq1 7442

Description: Equality theorem for nested function and operation value. Closed form of fvoveq1d 7441. (Contributed by AV, 23-Jul-2022.)

Assertion

Ref	Expression
fvoveq1	⊢ (𝐴 = 𝐵 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶)))

Proof of Theorem fvoveq1

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	fvoveq1d 7441	1 ⊢ (𝐴 = 𝐵 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶)))

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ‘cfv 6540  (class class class)co 7419

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422

This theorem is used by:  coof  7708  fldiv4p1lem1div2  13888  fldiv4lem1div2  13890  modval  13924  seqval  14068  seqp1  14072  seqshft2  14084  monoord  14088  monoord2  14089  seqhomo  14105  facp1  14334  faclbnd4lem2  14350  bcval  14360  lsw0  14622  ccatval1  14634  ccatval2  14635  ccatalpha  14652  swrdfv  14708  2swrd2eqwrdeq  15016  imval  15184  recan  15414  rlimcld2  15655  rlimcn1  15665  rlimcn3  15667  climcn1  15669  climcn2  15670  subcn2  15672  o1of2  15690  isercoll2  15746  climsup  15747  serf0  15758  iseraltlem2  15760  fsumrelem  15884  mertenslem1  15963  mertenslem2  15964  mertens  15965  bitsfval  16505  smuval  16563  pcfac  16983  vdwlem6  17070  vdwlem8  17072  vdwlem9  17073  vdwlem10  17074  imasaddvallem  17607  imasvscafn  17615  imasvscaval  17616  chnltm1  18689  chnind  18701  mgmhmlin  18791  mhmlin  18890  mhmlem  19174  mulginvcom  19211  mhmmulg  19227  ghmlin  19337  efgsdm  19846  efgsdmi  19848  efgsrel  19850  efgsp1  19853  frgpup1  19891  rnghmmul  20579  c0snmgmhm  20592  zrrnghm  20687  abvmul  20976  abvtri  20977  issrngd  21010  lmhmlin  21208  ipcj  21836  psrmulval  22146  mhpmulcl  22364  psdcoef  22375  psdadd  22378  psdpw  22385  coe1mul2  22482  coe1tmmul2fv  22491  coe1pwmulfv  22493  cply1mul  22508  mat1scmat  22748  mdetmul  22832  madufval  22846  cramer0  22899  cpmatmcllem  22927  d1mat2pmat  22948  m2cpminvid2lem  22963  decpmatmullem  22980  decpmatmulsumfsupp  22982  pm2mpmhmlem1  23027  pm2mpmhmlem2  23028  cayhamlem1  23075  cpmadumatpoly  23092  cayleyhamilton  23099  1stcelcls  23671  imasdsf1olem  24583  comet  24723  nrmmetd  24784  tngngp  24864  tngngp3  24866  nmvs  24886  mulc1cncf  25117  cncfco  25119  pi1xfr  25267  pi1coghm  25273  caubl  25520  caublcls  25521  bcthlem2  25537  bcthlem3  25538  bcthlem4  25539  bcthlem5  25540  ivthlem2  25664  ovolicc2lem4  25732  volsuplem  25767  volsup  25768  uniioombllem3  25797  itg1climres  25926  itg2monolem1  25962  itg2i1fseqle  25966  itg2i1fseq  25967  itg2i1fseq2  25968  itg2addlem  25970  itgeq2  25990  dvferm1lem  26196  dvferm2lem  26198  dvlip  26205  c1lip1  26209  lhop1lem  26225  lhop1  26226  ftc1lem4  26251  ftc1lem6  26253  mdegmullem  26288  coe1mul3  26309  ply1divex  26347  coeeu  26435  coeeq  26437  coemullem  26460  coemul  26462  plymulidp  26496  dvply1  26498  dvply2g  26499  aalioulem3  26550  aaliou3lem8  26561  ulmshftlem  26605  ulmshft  26606  ulmss  26613  pserdvlem2  26644  cxpcn3lem  26965  loglesqrt  26979  birthdaylem2  27170  emcllem2  27214  emcllem3  27215  harmonicbnd2  27222  lgamgulmlem2  27247  lgamgulmlem3  27248  lgamgulmlem5  27250  lgambdd  27254  lgamcvglem  27257  facgam  27283  ftalem7  27296  bposlem7  27507  bposlem9  27509  lgsqrlem2  27564  lgsqrlem4  27566  2lgslem3a  27613  2lgslem3b  27614  2lgslem3c  27615  2lgslem3d  27616  rplogsumlem1  27701  dchrvmasumlem1  27712  logsqvma  27759  logsqvma2  27760  selberglem3  27764  selberg  27765  selberg2lem  27767  selberg4lem1  27777  pntrsumo1  27782  selberg34r  27788  pntsval  27789  pntsval2  27793  pntrlog2bndlem1  27794  pntrlog2bndlem4  27797  pntpbnd  27805  pntibnd  27810  pntlemo  27824  addbday  28264  addonbday  28525  seqsval  28534  seqsp1  28557  bdaypw2n0bndlem  28709  ewlkinedg  30014  wkslem1  30017  uspgr2wlkeq  30055  wlkdlem2  30091  upgrwlkdvdelem  30151  crctcshwlkn0lem2  30229  crctcshwlkn0lem3  30230  crctcshwlkn0lem4  30231  crctcshwlkn0lem5  30232  wlkiswwlks2lem2  30288  wlkiswwlks2lem5  30291  wwlksnext  30311  wwlksnredwwlkn  30313  wwlksnextproplem2  30328  clwwlkccatlem  30409  clwlkclwwlklem2a1  30412  clwlkclwwlklem2fv1  30415  clwlkclwwlklem2a4  30417  clwlkclwwlklem2a  30418  clwlkclwwlklem2  30420  clwwisshclwwslemlem  30433  clwwisshclwws  30435  clwwlknlbonbgr1  30459  clwwlkel  30466  clwwlkf  30467  clwwlkwwlksb  30474  clwwlkext2edg  30476  wwlksext2clwwlk  30477  clwwlknonex2lem2  30528  eupthseg  30630  upgreupthseg  30633  eupth2lem3  30660  2clwwlk2clwwlklem  30770  2clwwlk  30771  numclwwlk1lem2f1  30781  numclwlk1lem2  30794  nvs  31088  nvtri  31095  ipval  31128  blocnilem  31229  phpar2  31248  phpar  31249  sii  31279  normsub0  31561  norm-ii  31563  norm-iii  31565  normsub  31568  normpyth  31570  norm3dif  31575  norm3lemt  31577  norm3adifi  31578  normpar  31580  polid  31584  bcs  31606  pjaddi  32111  pjsubi  32113  pjmuli  32114  pjcjt2  32117  lnopeq0lem2  32431  lnopunilem2  32436  branmfn  32530  hstel2  32644  stj  32660  cdj3lem1  32859  cdj3lem2b  32862  cdj3lem3b  32865  cdj3i  32866  ccatws1f1o  33339  gsummulsubdishift1  33454  elrgspnlem2  33629  selvply1rhmlemb  33975  constrsuc  34194  cnre2csqlem  34366  cnre2csqima  34367  mndpluscn  34382  lmdvg  34409  signsvfn  35036  subfacval2  35718  cvmliftlem7  35822  elmrsubrn  36051  faclim2  36279  fwddifval  36693  fwddifnval  36694  dnival  37119  unblimceq0lem  37154  unbdqndv2  37159  matunitlindf  38328  poimirlem32  38362  itg2gt0cn  38385  ftc1cnnclem  38401  ftc1cnnc  38402  areacirc  38423  sdclem1  38454  fdc  38456  seqpo  38458  incsequz  38459  incsequz2  38460  mettrifi  38468  caushft  38472  bfplem1  38533  ghomco  38602  rngohomadd  38680  rngohommul  38681  dihval  42066  lclkrlem1  42340  hdmap14lem2a  42701  hgmapval  42721  deg1pow  42968  sticksstones10  42982  sticksstones12a  42984  abvexp  43360  fsuppind  43382  prjspnval  43408  incssnn0  43502  rencldnfilem  43607  irrapxlem5  43613  irrapxlem6  43614  pellexlem3  43618  cvgdvgrat  45083  radcnvrat  45084  hashnzfzclim  45092  binomcxplemradcnv  45122  iunincfi  45872  monoords  46076  fperiodmullem  46082  monoordxrv  46255  monoordxr  46256  monoord2xrv  46257  monoord2xr  46258  climinf  46382  climsuse  46384  climinff  46387  mullimc  46392  mullimcf  46399  idlimc  46402  limcperiod  46404  limcrecl  46405  limclner  46425  climinf2  46481  climxrrelem  46523  cnrefiisplem  46603  cnrefiisp  46604  climxlim2lem  46619  cncfshift  46648  cncfperiod  46653  fperdvper  46693  dvnmul  46717  iblspltprt  46747  itgspltprt  46753  itgiccshift  46754  itgperiod  46755  dirkerval2  46868  dirkertrigeqlem1  46872  dirkertrigeqlem2  46873  dirkertrigeqlem3  46874  dirkercncflem2  46878  dirkercncflem3  46879  fourierdlem29  46910  fourierdlem48  46928  fourierdlem49  46929  fourierdlem113  46993  elaa2lem  47007  elaa2  47008  nnfoctbdj  47230  meaiuninclem  47254  meaiunincf  47257  meaiuninc3v  47258  meaiuninc3  47259  meaiininclem  47260  meaiininc  47261  smflimlem6  47550  ormkglobd  47651  natglobalincr  47653  2ltceilhalf  48129  ceilhalfnn  48137  smonoord  48174  iccpartimp  48226  iccelpart  48242  icceuelpart  48245  fargshiftfv  48248  fmtnorec2  48355  ppivalnnnprmge6  48438  ppivalnnnprm  48440  ppivalnn  48444  bgoldbtbndlem2  48631  bgoldbtbndlem3  48632  bgoldbtbnd  48634  upgrimwlklem5  48726  gpgov  48867  gpg5nbgrvtx13starlem2  48897  ply1mulgsumlem3  49227  ply1mulgsumlem4  49228  ply1mulgsum  49229  ackvalsuc1  49518