Theorem fvoveq1 7379

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

Syntax hints:   → wi 4   = wceq 1541  ‘cfv 6490  (class class class)co 7356

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498  df-ov 7359

This theorem is referenced by:  coof  7644  fldiv4p1lem1div2  13753  fldiv4lem1div2  13755  modval  13789  seqval  13933  seqp1  13937  seqshft2  13949  monoord  13953  monoord2  13954  seqhomo  13970  facp1  14199  faclbnd4lem2  14215  bcval  14225  lsw0  14486  ccatval1  14498  ccatval2  14499  ccatalpha  14515  swrdfv  14570  2swrd2eqwrdeq  14874  imval  15028  recan  15258  rlimcld2  15499  rlimcn1  15509  rlimcn3  15511  climcn1  15513  climcn2  15514  subcn2  15516  o1of2  15534  isercoll2  15590  climsup  15591  serf0  15602  iseraltlem2  15604  fsumrelem  15728  mertenslem1  15805  mertenslem2  15806  mertens  15807  bitsfval  16348  smuval  16406  pcfac  16825  vdwlem6  16912  vdwlem8  16914  vdwlem9  16915  vdwlem10  16916  imasaddvallem  17448  imasvscafn  17456  imasvscaval  17457  chnltm1  18530  chnind  18542  mgmhmlin  18622  mhmlin  18716  mhmlem  18990  mulginvcom  19027  mhmmulg  19043  ghmlin  19148  efgsdm  19657  efgsdmi  19659  efgsrel  19661  efgsp1  19664  frgpup1  19702  rnghmmul  20383  c0snmgmhm  20396  zrrnghm  20467  abvmul  20752  abvtri  20753  issrngd  20786  lmhmlin  20985  ipcj  21587  psrmulval  21898  mhpmulcl  22090  psdcoef  22101  psdadd  22104  psdpw  22111  coe1mul2  22209  coe1tmmul2fv  22218  coe1pwmulfv  22220  cply1mul  22238  mat1scmat  22481  mdetmul  22565  madufval  22579  cramer0  22632  cpmatmcllem  22660  d1mat2pmat  22681  m2cpminvid2lem  22696  decpmatmullem  22713  decpmatmulsumfsupp  22715  pm2mpmhmlem1  22760  pm2mpmhmlem2  22761  cayhamlem1  22808  cpmadumatpoly  22825  cayleyhamilton  22832  1stcelcls  23403  imasdsf1olem  24315  comet  24455  nrmmetd  24516  tngngp  24596  tngngp3  24598  nmvs  24618  mulc1cncf  24852  cncfco  24854  pi1xfr  25009  pi1coghm  25015  caubl  25262  caublcls  25263  bcthlem2  25279  bcthlem3  25280  bcthlem4  25281  bcthlem5  25282  ivthlem2  25407  ovolicc2lem4  25475  volsuplem  25510  volsup  25511  uniioombllem3  25540  itg1climres  25669  itg2monolem1  25705  itg2i1fseqle  25709  itg2i1fseq  25710  itg2i1fseq2  25711  itg2addlem  25713  itgeq2  25733  dvferm1lem  25942  dvferm2lem  25944  dvlip  25952  c1lip1  25956  lhop1lem  25972  lhop1  25973  ftc1lem4  26000  ftc1lem6  26002  mdegmullem  26037  coe1mul3  26058  ply1divex  26096  coeeu  26184  coeeq  26186  coemullem  26209  coemul  26211  dvply1  26245  dvply2g  26246  dvply2gOLD  26247  aalioulem3  26296  aaliou3lem8  26307  ulmshftlem  26352  ulmshft  26353  ulmss  26360  pserdvlem2  26392  cxpcn3lem  26711  loglesqrt  26725  birthdaylem2  26916  emcllem2  26961  emcllem3  26962  harmonicbnd2  26969  lgamgulmlem2  26994  lgamgulmlem3  26995  lgamgulmlem5  26997  lgambdd  27001  lgamcvglem  27004  facgam  27030  ftalem7  27043  bposlem7  27255  bposlem9  27257  lgsqrlem2  27312  lgsqrlem4  27314  2lgslem3a  27361  2lgslem3b  27362  2lgslem3c  27363  2lgslem3d  27364  rplogsumlem1  27449  dchrvmasumlem1  27460  logsqvma  27507  logsqvma2  27508  selberglem3  27512  selberg  27513  selberg2lem  27515  selberg4lem1  27525  pntrsumo1  27530  selberg34r  27536  pntsval  27537  pntsval2  27541  pntrlog2bndlem1  27542  pntrlog2bndlem4  27545  pntpbnd  27553  pntibnd  27558  pntlemo  27572  addsbday  27987  seqsval  28249  seqsp1  28272  bdaypw2n0s  28420  zs12bday  28433  ewlkinedg  29627  wkslem1  29630  uspgr2wlkeq  29668  wlkdlem2  29704  upgrwlkdvdelem  29758  crctcshwlkn0lem2  29833  crctcshwlkn0lem3  29834  crctcshwlkn0lem4  29835  crctcshwlkn0lem5  29836  wlkiswwlks2lem2  29892  wlkiswwlks2lem5  29895  wwlksnext  29915  wwlksnredwwlkn  29917  wwlksnextproplem2  29932  clwwlkccatlem  30013  clwlkclwwlklem2a1  30016  clwlkclwwlklem2fv1  30019  clwlkclwwlklem2a4  30021  clwlkclwwlklem2a  30022  clwlkclwwlklem2  30024  clwwisshclwwslemlem  30037  clwwisshclwws  30039  clwwlknlbonbgr1  30063  clwwlkel  30070  clwwlkf  30071  clwwlkwwlksb  30078  clwwlkext2edg  30080  wwlksext2clwwlk  30081  clwwlknonex2lem2  30132  eupthseg  30230  upgreupthseg  30233  eupth2lem3  30260  2clwwlk2clwwlklem  30370  2clwwlk  30371  numclwwlk1lem2f1  30381  numclwlk1lem2  30394  nvs  30687  nvtri  30694  ipval  30727  blocnilem  30828  phpar2  30847  phpar  30848  sii  30878  normsub0  31160  norm-ii  31162  norm-iii  31164  normsub  31167  normpyth  31169  norm3dif  31174  norm3lemt  31176  norm3adifi  31177  normpar  31179  polid  31183  bcs  31205  pjaddi  31710  pjsubi  31712  pjmuli  31713  pjcjt2  31716  lnopeq0lem2  32030  lnopunilem2  32035  branmfn  32129  hstel2  32243  stj  32259  cdj3lem1  32458  cdj3lem2b  32461  cdj3lem3b  32464  cdj3i  32465  ccatws1f1o  32982  gsummulsubdishift1  33100  elrgspnlem2  33274  constrsuc  33844  cnre2csqlem  34016  cnre2csqima  34017  mndpluscn  34032  lmdvg  34059  plymulx  34654  signsvfn  34688  subfacval2  35330  cvmliftlem7  35434  elmrsubrn  35663  faclim2  35891  fwddifval  36305  fwddifnval  36306  dnival  36614  unblimceq0lem  36649  unbdqndv2  36654  matunitlindf  37758  poimirlem32  37792  itg2gt0cn  37815  ftc1cnnclem  37831  ftc1cnnc  37832  areacirc  37853  sdclem1  37883  fdc  37885  seqpo  37887  incsequz  37888  incsequz2  37889  mettrifi  37897  caushft  37901  bfplem1  37962  ghomco  38031  rngohomadd  38109  rngohommul  38110  dihval  41431  lclkrlem1  41705  hdmap14lem2a  42066  hgmapval  42086  deg1pow  42334  sticksstones10  42348  sticksstones12a  42350  abvexp  42729  fsuppind  42775  prjspnval  42801  incssnn0  42895  rencldnfilem  43004  irrapxlem5  43010  irrapxlem6  43011  pellexlem3  43015  cvgdvgrat  44496  radcnvrat  44497  hashnzfzclim  44505  binomcxplemradcnv  44535  iunincfi  45280  monoords  45487  fperiodmullem  45493  monoordxrv  45667  monoordxr  45668  monoord2xrv  45669  monoord2xr  45670  climinf  45794  climsuse  45796  climinff  45799  mullimc  45804  mullimcf  45811  idlimc  45814  limcperiod  45816  limcrecl  45817  limclner  45837  climinf2  45893  climxrrelem  45935  cnrefiisplem  46015  cnrefiisp  46016  climxlim2lem  46031  cncfshift  46060  cncfperiod  46065  fperdvper  46105  dvnmul  46129  iblspltprt  46159  itgspltprt  46165  itgiccshift  46166  itgperiod  46167  dirkerval2  46280  dirkertrigeqlem1  46284  dirkertrigeqlem2  46285  dirkertrigeqlem3  46286  dirkercncflem2  46290  dirkercncflem3  46291  fourierdlem29  46322  elaa2lem  46419  elaa2  46420  nnfoctbdj  46642  meaiuninclem  46666  meaiunincf  46669  meaiuninc3v  46670  meaiuninc3  46671  meaiininclem  46672  meaiininc  46673  smflimlem6  46962  ormkglobd  47061  natglobalincr  47063  2ltceilhalf  47516  ceilhalfnn  47524  smonoord  47559  iccpartimp  47605  iccelpart  47621  icceuelpart  47624  fargshiftfv  47627  fmtnorec2  47731  bgoldbtbndlem2  47994  bgoldbtbndlem3  47995  bgoldbtbnd  47997  upgrimwlklem5  48089  gpgov  48230  gpg5nbgrvtx13starlem2  48260  ply1mulgsumlem3  48576  ply1mulgsumlem4  48577  ply1mulgsum  48578  ackvalsuc1  48867