Theorem fvoveq1 7410

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

Syntax hints:   → wi 4   = wceq 1540  ‘cfv 6511  (class class class)co 7387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390

This theorem is referenced by:  coof  7677  eluzaddOLD  12828  eluzsubOLD  12829  fldiv4p1lem1div2  13797  fldiv4lem1div2  13799  modval  13833  seqval  13977  seqp1  13981  seqshft2  13993  monoord  13997  monoord2  13998  seqhomo  14014  facp1  14243  faclbnd4lem2  14259  bcval  14269  lsw0  14530  ccatval1  14542  ccatval2  14543  ccatalpha  14558  swrdfv  14613  2swrd2eqwrdeq  14919  imval  15073  recan  15303  rlimcld2  15544  rlimcn1  15554  rlimcn3  15556  climcn1  15558  climcn2  15559  subcn2  15561  o1of2  15579  isercoll2  15635  climsup  15636  serf0  15647  iseraltlem2  15649  fsumrelem  15773  mertenslem1  15850  mertenslem2  15851  mertens  15852  bitsfval  16393  smuval  16451  pcfac  16870  vdwlem6  16957  vdwlem8  16959  vdwlem9  16960  vdwlem10  16961  imasaddvallem  17492  imasvscafn  17500  imasvscaval  17501  mgmhmlin  18626  mhmlin  18720  mhmlem  18994  mulginvcom  19031  mhmmulg  19047  ghmlin  19153  efgsdm  19660  efgsdmi  19662  efgsrel  19664  efgsp1  19667  frgpup1  19705  rnghmmul  20358  c0snmgmhm  20371  zrrnghm  20445  abvmul  20730  abvtri  20731  issrngd  20764  lmhmlin  20942  ipcj  21543  psrmulval  21853  mhpmulcl  22036  psdcoef  22047  psdadd  22050  psdpw  22057  coe1mul2  22155  coe1tmmul2fv  22164  coe1pwmulfv  22166  cply1mul  22183  mat1scmat  22426  mdetmul  22510  madufval  22524  cramer0  22577  cpmatmcllem  22605  d1mat2pmat  22626  m2cpminvid2lem  22641  decpmatmullem  22658  decpmatmulsumfsupp  22660  pm2mpmhmlem1  22705  pm2mpmhmlem2  22706  cayhamlem1  22753  cpmadumatpoly  22770  cayleyhamilton  22777  1stcelcls  23348  imasdsf1olem  24261  comet  24401  nrmmetd  24462  tngngp  24542  tngngp3  24544  nmvs  24564  mulc1cncf  24798  cncfco  24800  pi1xfr  24955  pi1coghm  24961  caubl  25208  caublcls  25209  bcthlem2  25225  bcthlem3  25226  bcthlem4  25227  bcthlem5  25228  ivthlem2  25353  ovolicc2lem4  25421  volsuplem  25456  volsup  25457  uniioombllem3  25486  itg1climres  25615  itg2monolem1  25651  itg2i1fseqle  25655  itg2i1fseq  25656  itg2i1fseq2  25657  itg2addlem  25659  itgeq2  25679  dvferm1lem  25888  dvferm2lem  25890  dvlip  25898  c1lip1  25902  lhop1lem  25918  lhop1  25919  ftc1lem4  25946  ftc1lem6  25948  mdegmullem  25983  coe1mul3  26004  ply1divex  26042  coeeu  26130  coeeq  26132  coemullem  26155  coemul  26157  dvply1  26191  dvply2g  26192  dvply2gOLD  26193  aalioulem3  26242  aaliou3lem8  26253  ulmshftlem  26298  ulmshft  26299  ulmss  26306  pserdvlem2  26338  cxpcn3lem  26657  loglesqrt  26671  birthdaylem2  26862  emcllem2  26907  emcllem3  26908  harmonicbnd2  26915  lgamgulmlem2  26940  lgamgulmlem3  26941  lgamgulmlem5  26943  lgambdd  26947  lgamcvglem  26950  facgam  26976  ftalem7  26989  bposlem7  27201  bposlem9  27203  lgsqrlem2  27258  lgsqrlem4  27260  2lgslem3a  27307  2lgslem3b  27308  2lgslem3c  27309  2lgslem3d  27310  rplogsumlem1  27395  dchrvmasumlem1  27406  logsqvma  27453  logsqvma2  27454  selberglem3  27458  selberg  27459  selberg2lem  27461  selberg4lem1  27471  pntrsumo1  27476  selberg34r  27482  pntsval  27483  pntsval2  27487  pntrlog2bndlem1  27488  pntrlog2bndlem4  27491  pntpbnd  27499  pntibnd  27504  pntlemo  27518  addsbday  27924  seqsval  28182  seqsp1  28205  zs12bday  28343  ewlkinedg  29532  wkslem1  29535  uspgr2wlkeq  29574  wlkdlem2  29611  upgrwlkdvdelem  29666  crctcshwlkn0lem2  29741  crctcshwlkn0lem3  29742  crctcshwlkn0lem4  29743  crctcshwlkn0lem5  29744  wlkiswwlks2lem2  29800  wlkiswwlks2lem5  29803  wwlksnext  29823  wwlksnredwwlkn  29825  wwlksnextproplem2  29840  clwwlkccatlem  29918  clwlkclwwlklem2a1  29921  clwlkclwwlklem2fv1  29924  clwlkclwwlklem2a4  29926  clwlkclwwlklem2a  29927  clwlkclwwlklem2  29929  clwwisshclwwslemlem  29942  clwwisshclwws  29944  clwwlknlbonbgr1  29968  clwwlkel  29975  clwwlkf  29976  clwwlkwwlksb  29983  clwwlkext2edg  29985  wwlksext2clwwlk  29986  clwwlknonex2lem2  30037  eupthseg  30135  upgreupthseg  30138  eupth2lem3  30165  2clwwlk2clwwlklem  30275  2clwwlk  30276  numclwwlk1lem2f1  30286  numclwlk1lem2  30299  nvs  30592  nvtri  30599  ipval  30632  blocnilem  30733  phpar2  30752  phpar  30753  sii  30783  normsub0  31065  norm-ii  31067  norm-iii  31069  normsub  31072  normpyth  31074  norm3dif  31079  norm3lemt  31081  norm3adifi  31082  normpar  31084  polid  31088  bcs  31110  pjaddi  31615  pjsubi  31617  pjmuli  31618  pjcjt2  31621  lnopeq0lem2  31935  lnopunilem2  31940  branmfn  32034  hstel2  32148  stj  32164  cdj3lem1  32363  cdj3lem2b  32366  cdj3lem3b  32369  cdj3i  32370  ccatws1f1o  32873  chnltm1  32934  chnind  32937  elrgspnlem2  33194  constrsuc  33728  cnre2csqlem  33900  cnre2csqima  33901  mndpluscn  33916  lmdvg  33943  plymulx  34539  signsvfn  34573  subfacval2  35174  cvmliftlem7  35278  elmrsubrn  35507  faclim2  35735  fwddifval  36150  fwddifnval  36151  dnival  36459  unblimceq0lem  36494  unbdqndv2  36499  matunitlindf  37612  poimirlem32  37646  itg2gt0cn  37669  ftc1cnnclem  37685  ftc1cnnc  37686  areacirc  37707  sdclem1  37737  fdc  37739  seqpo  37741  incsequz  37742  incsequz2  37743  mettrifi  37751  caushft  37755  bfplem1  37816  ghomco  37885  rngohomadd  37963  rngohommul  37964  dihval  41226  lclkrlem1  41500  hdmap14lem2a  41861  hgmapval  41881  deg1pow  42129  sticksstones10  42143  sticksstones12a  42145  abvexp  42520  fsuppind  42578  prjspnval  42604  incssnn0  42699  rencldnfilem  42808  irrapxlem5  42814  irrapxlem6  42815  pellexlem3  42819  cvgdvgrat  44302  radcnvrat  44303  hashnzfzclim  44311  binomcxplemradcnv  44341  iunincfi  45088  monoords  45295  fperiodmullem  45301  monoordxrv  45477  monoordxr  45478  monoord2xrv  45479  monoord2xr  45480  climinf  45604  climsuse  45606  climinff  45609  mullimc  45614  mullimcf  45621  idlimc  45624  limcperiod  45626  limcrecl  45627  limclner  45649  climinf2  45705  climxrrelem  45747  cnrefiisplem  45827  cnrefiisp  45828  climxlim2lem  45843  cncfshift  45872  cncfperiod  45877  fperdvper  45917  dvnmul  45941  iblspltprt  45971  itgspltprt  45977  itgiccshift  45978  itgperiod  45979  dirkerval2  46092  dirkertrigeqlem1  46096  dirkertrigeqlem2  46097  dirkertrigeqlem3  46098  dirkercncflem2  46102  dirkercncflem3  46103  fourierdlem29  46134  elaa2lem  46231  elaa2  46232  nnfoctbdj  46454  meaiuninclem  46478  meaiunincf  46481  meaiuninc3v  46482  meaiuninc3  46483  meaiininclem  46484  meaiininc  46485  smflimlem6  46774  ormkglobd  46873  natglobalincr  46875  tworepnotupword  46884  2ltceilhalf  47329  ceilhalfnn  47337  smonoord  47372  iccpartimp  47418  iccelpart  47434  icceuelpart  47437  fargshiftfv  47440  fmtnorec2  47544  bgoldbtbndlem2  47807  bgoldbtbndlem3  47808  bgoldbtbnd  47810  upgrimwlklem5  47901  gpgov  48033  gpg5nbgrvtx13starlem2  48063  ply1mulgsumlem3  48377  ply1mulgsumlem4  48378  ply1mulgsum  48379  ackvalsuc1  48668