Theorem fvoveq1 7291

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

Assertion

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

Proof of Theorem fvoveq1

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

Syntax hints:   → wi 4   = wceq 1541  ‘cfv 6430  (class class class)co 7268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-iota 6388  df-fv 6438  df-ov 7271

This theorem is referenced by:  eluzadd  12595  eluzsub  12596  fldiv4p1lem1div2  13536  fldiv4lem1div2  13538  modval  13572  seqval  13713  seqp1  13717  seqshft2  13730  monoord  13734  monoord2  13735  seqhomo  13751  facp1  13973  faclbnd4lem2  13989  bcval  13999  lsw0  14249  ccatval1  14262  ccatval1OLD  14263  ccatval2  14264  ccatalpha  14279  swrdfv  14342  2swrd2eqwrdeq  14647  imval  14799  recan  15029  rlimcld2  15268  rlimcn1  15278  rlimcn3  15280  climcn1  15282  climcn2  15283  subcn2  15285  o1of2  15303  isercoll2  15361  climsup  15362  serf0  15373  iseraltlem2  15375  fsumrelem  15500  mertenslem1  15577  mertenslem2  15578  mertens  15579  bitsfval  16111  smuval  16169  pcfac  16581  vdwlem6  16668  vdwlem8  16670  vdwlem9  16671  vdwlem10  16672  imasaddvallem  17221  imasvscafn  17229  imasvscaval  17230  mhmlin  18418  mhmlem  18676  mulginvcom  18709  mhmmulg  18725  ghmlin  18820  efgsdm  19317  efgsdmi  19319  efgsrel  19321  efgsp1  19324  frgpup1  19362  abvmul  20070  abvtri  20071  issrngd  20102  lmhmlin  20278  ipcj  20820  psrmulval  21136  mhpmulcl  21320  coe1mul2  21421  coe1tmmul2fv  21430  coe1pwmulfv  21432  cply1mul  21446  mat1scmat  21669  mdetmul  21753  madufval  21767  cramer0  21820  cpmatmcllem  21848  d1mat2pmat  21869  m2cpminvid2lem  21884  decpmatmullem  21901  decpmatmulsumfsupp  21903  pm2mpmhmlem1  21948  pm2mpmhmlem2  21949  cayhamlem1  21996  cpmadumatpoly  22013  cayleyhamilton  22020  1stcelcls  22593  imasdsf1olem  23507  comet  23650  nrmmetd  23711  tngngp  23799  tngngp3  23801  nmvs  23821  mulc1cncf  24049  cncfco  24051  pi1xfr  24199  pi1coghm  24205  caubl  24453  caublcls  24454  bcthlem2  24470  bcthlem3  24471  bcthlem4  24472  bcthlem5  24473  ivthlem2  24597  ovolicc2lem4  24665  volsuplem  24700  volsup  24701  uniioombllem3  24730  itg1climres  24860  itg2monolem1  24896  itg2i1fseqle  24900  itg2i1fseq  24901  itg2i1fseq2  24902  itg2addlem  24904  itgeq2  24923  dvferm1lem  25129  dvferm2lem  25131  dvlip  25138  c1lip1  25142  lhop1lem  25158  lhop1  25159  ftc1lem4  25184  ftc1lem6  25186  mdegmullem  25224  coe1mul3  25245  ply1divex  25282  coeeu  25367  coeeq  25369  coemullem  25392  coemul  25394  dvply1  25425  dvply2g  25426  aalioulem3  25475  aaliou3lem8  25486  ulmshftlem  25529  ulmshft  25530  ulmss  25537  pserdvlem2  25568  cxpcn3lem  25881  loglesqrt  25892  birthdaylem2  26083  emcllem2  26127  emcllem3  26128  harmonicbnd2  26135  lgamgulmlem2  26160  lgamgulmlem3  26161  lgamgulmlem5  26163  lgambdd  26167  lgamcvglem  26170  facgam  26196  ftalem7  26209  bposlem7  26419  bposlem9  26421  lgsqrlem2  26476  lgsqrlem4  26478  2lgslem3a  26525  2lgslem3b  26526  2lgslem3c  26527  2lgslem3d  26528  rplogsumlem1  26613  dchrvmasumlem1  26624  logsqvma  26671  logsqvma2  26672  selberglem3  26676  selberg  26677  selberg2lem  26679  selberg4lem1  26689  pntrsumo1  26694  selberg34r  26700  pntsval  26701  pntsval2  26705  pntrlog2bndlem1  26706  pntrlog2bndlem4  26709  pntpbnd  26717  pntibnd  26722  pntlemo  26736  ewlkinedg  27952  wkslem1  27955  uspgr2wlkeq  27993  wlkdlem2  28031  upgrwlkdvdelem  28083  crctcshwlkn0lem2  28155  crctcshwlkn0lem3  28156  crctcshwlkn0lem4  28157  crctcshwlkn0lem5  28158  wlkiswwlks2lem2  28214  wlkiswwlks2lem5  28217  wwlksnext  28237  wwlksnredwwlkn  28239  wwlksnextproplem2  28254  clwwlkccatlem  28332  clwlkclwwlklem2a1  28335  clwlkclwwlklem2fv1  28338  clwlkclwwlklem2a4  28340  clwlkclwwlklem2a  28341  clwlkclwwlklem2  28343  clwwisshclwwslemlem  28356  clwwisshclwws  28358  clwwlknlbonbgr1  28382  clwwlkel  28389  clwwlkf  28390  clwwlkwwlksb  28397  clwwlkext2edg  28399  wwlksext2clwwlk  28400  clwwlknonex2lem2  28451  eupthseg  28549  upgreupthseg  28552  eupth2lem3  28579  2clwwlk2clwwlklem  28689  2clwwlk  28690  numclwwlk1lem2f1  28700  numclwlk1lem2  28713  nvs  29004  nvtri  29011  ipval  29044  blocnilem  29145  phpar2  29164  phpar  29165  sii  29195  normsub0  29477  norm-ii  29479  norm-iii  29481  normsub  29484  normpyth  29486  norm3dif  29491  norm3lemt  29493  norm3adifi  29494  normpar  29496  polid  29500  bcs  29522  pjaddi  30027  pjsubi  30029  pjmuli  30030  pjcjt2  30033  lnopeq0lem2  30347  lnopunilem2  30352  branmfn  30446  hstel2  30560  stj  30576  cdj3lem1  30775  cdj3lem2b  30778  cdj3lem3b  30781  cdj3i  30782  cnre2csqlem  31839  cnre2csqima  31840  mndpluscn  31855  lmdvg  31882  plymulx  32506  signsvfn  32540  subfacval2  33128  cvmliftlem7  33232  elmrsubrn  33461  faclim2  33693  fwddifval  34443  fwddifnval  34444  dnival  34630  unblimceq0lem  34665  unbdqndv2  34670  matunitlindf  35754  poimirlem32  35788  itg2gt0cn  35811  ftc1cnnclem  35827  ftc1cnnc  35828  areacirc  35849  sdclem1  35880  fdc  35882  seqpo  35884  incsequz  35885  incsequz2  35886  mettrifi  35894  caushft  35898  bfplem1  35959  ghomco  36028  rngohomadd  36106  rngohommul  36107  dihval  39225  lclkrlem1  39499  hdmap14lem2a  39860  hgmapval  39880  sticksstones10  40091  sticksstones12a  40093  fsuppind  40259  prjspnval  40435  incssnn0  40513  rencldnfilem  40622  irrapxlem5  40628  irrapxlem6  40629  pellexlem3  40633  cvgdvgrat  41884  radcnvrat  41885  hashnzfzclim  41893  binomcxplemradcnv  41923  iunincfi  42597  monoords  42790  fperiodmullem  42796  monoordxrv  42976  monoordxr  42977  monoord2xrv  42978  monoord2xr  42979  climinf  43101  climsuse  43103  climinff  43106  mullimc  43111  mullimcf  43118  idlimc  43121  limcperiod  43123  limcrecl  43124  limclner  43146  climinf2  43202  climxrrelem  43244  cnrefiisplem  43324  cnrefiisp  43325  climxlim2lem  43340  cncfshift  43369  cncfperiod  43374  fperdvper  43414  dvnmul  43438  iblspltprt  43468  itgspltprt  43474  itgiccshift  43475  itgperiod  43476  dirkerval2  43589  dirkertrigeqlem1  43593  dirkertrigeqlem2  43594  dirkertrigeqlem3  43595  dirkercncflem2  43599  dirkercncflem3  43600  fourierdlem29  43631  elaa2lem  43728  elaa2  43729  nnfoctbdj  43948  meaiuninclem  43972  meaiunincf  43975  meaiuninc3v  43976  meaiuninc3  43977  meaiininclem  43978  meaiininc  43979  smflimlem6  44262  smonoord  44775  iccpartimp  44821  iccelpart  44837  icceuelpart  44840  fargshiftfv  44843  fmtnorec2  44947  bgoldbtbndlem2  45210  bgoldbtbndlem3  45211  bgoldbtbnd  45213  mgmhmlin  45292  rnghmmul  45410  c0snmgmhm  45424  zrrnghm  45427  ply1mulgsumlem3  45681  ply1mulgsumlem4  45682  ply1mulgsum  45683  ackvalsuc1  45977