Theorem fvoveq1 7433

Description: Equality theorem for nested function and operation value. Closed form of fvoveq1d 7432. (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 7432	1 ⊢ (𝐴 = 𝐵 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶)))

Syntax hints:   → wi 4   = wceq 1570  ‘cfv 6536  (class class class)co 7410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413

This theorem is referenced by:  coof  7698  fldiv4p1lem1div2  13864  fldiv4lem1div2  13866  modval  13900  seqval  14044  seqp1  14048  seqshft2  14060  monoord  14064  monoord2  14065  seqhomo  14081  facp1  14310  faclbnd4lem2  14326  bcval  14336  lsw0  14598  ccatval1  14610  ccatval2  14611  ccatalpha  14627  swrdfv  14682  2swrd2eqwrdeq  14986  imval  15154  recan  15384  rlimcld2  15625  rlimcn1  15635  rlimcn3  15637  climcn1  15639  climcn2  15640  subcn2  15642  o1of2  15660  isercoll2  15716  climsup  15717  serf0  15728  iseraltlem2  15730  fsumrelem  15855  mertenslem1  15934  mertenslem2  15935  mertens  15936  bitsfval  16476  smuval  16534  pcfac  16954  vdwlem6  17041  vdwlem8  17043  vdwlem9  17044  vdwlem10  17045  imasaddvallem  17578  imasvscafn  17586  imasvscaval  17587  chnltm1  18660  chnind  18672  mgmhmlin  18752  mhmlin  18846  mhmlem  19123  mulginvcom  19160  mhmmulg  19176  ghmlin  19286  efgsdm  19795  efgsdmi  19797  efgsrel  19799  efgsp1  19802  frgpup1  19840  rnghmmul  20527  c0snmgmhm  20540  zrrnghm  20635  abvmul  20924  abvtri  20925  issrngd  20958  lmhmlin  21156  ipcj  21784  psrmulval  22094  mhpmulcl  22312  psdcoef  22323  psdadd  22326  psdpw  22333  coe1mul2  22430  coe1tmmul2fv  22439  coe1pwmulfv  22441  cply1mul  22456  mat1scmat  22696  mdetmul  22780  madufval  22794  cramer0  22847  cpmatmcllem  22875  d1mat2pmat  22896  m2cpminvid2lem  22911  decpmatmullem  22928  decpmatmulsumfsupp  22930  pm2mpmhmlem1  22975  pm2mpmhmlem2  22976  cayhamlem1  23023  cpmadumatpoly  23040  cayleyhamilton  23047  1stcelcls  23618  imasdsf1olem  24530  comet  24670  nrmmetd  24731  tngngp  24811  tngngp3  24813  nmvs  24833  mulc1cncf  25064  cncfco  25066  pi1xfr  25214  pi1coghm  25220  caubl  25467  caublcls  25468  bcthlem2  25484  bcthlem3  25485  bcthlem4  25486  bcthlem5  25487  ivthlem2  25611  ovolicc2lem4  25679  volsuplem  25714  volsup  25715  uniioombllem3  25744  itg1climres  25873  itg2monolem1  25909  itg2i1fseqle  25913  itg2i1fseq  25914  itg2i1fseq2  25915  itg2addlem  25917  itgeq2  25937  dvferm1lem  26143  dvferm2lem  26145  dvlip  26152  c1lip1  26156  lhop1lem  26172  lhop1  26173  ftc1lem4  26198  ftc1lem6  26200  mdegmullem  26235  coe1mul3  26256  ply1divex  26294  coeeu  26382  coeeq  26384  coemullem  26407  coemul  26409  plymulidp  26443  dvply1  26445  dvply2g  26446  aalioulem3  26497  aaliou3lem8  26508  ulmshftlem  26552  ulmshft  26553  ulmss  26560  pserdvlem2  26591  cxpcn3lem  26912  loglesqrt  26926  birthdaylem2  27117  emcllem2  27161  emcllem3  27162  harmonicbnd2  27169  lgamgulmlem2  27194  lgamgulmlem3  27195  lgamgulmlem5  27197  lgambdd  27201  lgamcvglem  27204  facgam  27230  ftalem7  27243  bposlem7  27454  bposlem9  27456  lgsqrlem2  27511  lgsqrlem4  27513  2lgslem3a  27560  2lgslem3b  27561  2lgslem3c  27562  2lgslem3d  27563  rplogsumlem1  27648  dchrvmasumlem1  27659  logsqvma  27706  logsqvma2  27707  selberglem3  27711  selberg  27712  selberg2lem  27714  selberg4lem1  27724  pntrsumo1  27729  selberg34r  27735  pntsval  27736  pntsval2  27740  pntrlog2bndlem1  27741  pntrlog2bndlem4  27744  pntpbnd  27752  pntibnd  27757  pntlemo  27771  addbday  28211  addonbday  28472  seqsval  28481  seqsp1  28504  bdaypw2n0bndlem  28656  ewlkinedg  29954  wkslem1  29957  uspgr2wlkeq  29995  wlkdlem2  30031  upgrwlkdvdelem  30085  crctcshwlkn0lem2  30160  crctcshwlkn0lem3  30161  crctcshwlkn0lem4  30162  crctcshwlkn0lem5  30163  wlkiswwlks2lem2  30219  wlkiswwlks2lem5  30222  wwlksnext  30242  wwlksnredwwlkn  30244  wwlksnextproplem2  30259  clwwlkccatlem  30340  clwlkclwwlklem2a1  30343  clwlkclwwlklem2fv1  30346  clwlkclwwlklem2a4  30348  clwlkclwwlklem2a  30349  clwlkclwwlklem2  30351  clwwisshclwwslemlem  30364  clwwisshclwws  30366  clwwlknlbonbgr1  30390  clwwlkel  30397  clwwlkf  30398  clwwlkwwlksb  30405  clwwlkext2edg  30407  wwlksext2clwwlk  30408  clwwlknonex2lem2  30459  eupthseg  30557  upgreupthseg  30560  eupth2lem3  30587  2clwwlk2clwwlklem  30697  2clwwlk  30698  numclwwlk1lem2f1  30708  numclwlk1lem2  30721  nvs  31015  nvtri  31022  ipval  31055  blocnilem  31156  phpar2  31175  phpar  31176  sii  31206  normsub0  31488  norm-ii  31490  norm-iii  31492  normsub  31495  normpyth  31497  norm3dif  31502  norm3lemt  31504  norm3adifi  31505  normpar  31507  polid  31511  bcs  31533  pjaddi  32038  pjsubi  32040  pjmuli  32041  pjcjt2  32044  lnopeq0lem2  32358  lnopunilem2  32363  branmfn  32457  hstel2  32571  stj  32587  cdj3lem1  32786  cdj3lem2b  32789  cdj3lem3b  32792  cdj3i  32793  ccatws1f1o  33271  gsummulsubdishift1  33388  elrgspnlem2  33563  selvply1rhmlemb  33909  constrsuc  34128  cnre2csqlem  34300  cnre2csqima  34301  mndpluscn  34316  lmdvg  34343  signsvfn  34969  subfacval2  35679  cvmliftlem7  35783  elmrsubrn  36012  faclim2  36240  fwddifval  36654  fwddifnval  36655  dnival  37080  unblimceq0lem  37115  unbdqndv2  37120  matunitlindf  38289  poimirlem32  38323  itg2gt0cn  38346  ftc1cnnclem  38362  ftc1cnnc  38363  areacirc  38384  sdclem1  38414  fdc  38416  seqpo  38418  incsequz  38419  incsequz2  38420  mettrifi  38428  caushft  38432  bfplem1  38493  ghomco  38562  rngohomadd  38640  rngohommul  38641  dihval  42026  lclkrlem1  42300  hdmap14lem2a  42661  hgmapval  42681  deg1pow  42928  sticksstones10  42942  sticksstones12a  42944  abvexp  43320  fsuppind  43342  prjspnval  43368  incssnn0  43462  rencldnfilem  43567  irrapxlem5  43573  irrapxlem6  43574  pellexlem3  43578  cvgdvgrat  45043  radcnvrat  45044  hashnzfzclim  45052  binomcxplemradcnv  45082  iunincfi  45832  monoords  46036  fperiodmullem  46042  monoordxrv  46215  monoordxr  46216  monoord2xrv  46217  monoord2xr  46218  climinf  46342  climsuse  46344  climinff  46347  mullimc  46352  mullimcf  46359  idlimc  46362  limcperiod  46364  limcrecl  46365  limclner  46385  climinf2  46441  climxrrelem  46483  cnrefiisplem  46563  cnrefiisp  46564  climxlim2lem  46579  cncfshift  46608  cncfperiod  46613  fperdvper  46653  dvnmul  46677  iblspltprt  46707  itgspltprt  46713  itgiccshift  46714  itgperiod  46715  dirkerval2  46828  dirkertrigeqlem1  46832  dirkertrigeqlem2  46833  dirkertrigeqlem3  46834  dirkercncflem2  46838  dirkercncflem3  46839  fourierdlem29  46870  fourierdlem48  46888  fourierdlem49  46889  fourierdlem113  46953  elaa2lem  46967  elaa2  46968  nnfoctbdj  47190  meaiuninclem  47214  meaiunincf  47217  meaiuninc3v  47218  meaiuninc3  47219  meaiininclem  47220  meaiininc  47221  smflimlem6  47510  ormkglobd  47611  natglobalincr  47613  2ltceilhalf  48089  ceilhalfnn  48097  smonoord  48134  iccpartimp  48186  iccelpart  48202  icceuelpart  48205  fargshiftfv  48208  fmtnorec2  48315  ppivalnnnprmge6  48398  ppivalnnnprm  48400  ppivalnn  48404  bgoldbtbndlem2  48591  bgoldbtbndlem3  48592  bgoldbtbnd  48594  upgrimwlklem5  48686  gpgov  48827  gpg5nbgrvtx13starlem2  48857  ply1mulgsumlem3  49188  ply1mulgsumlem4  49189  ply1mulgsum  49190  ackvalsuc1  49479