Theorem fvoveq1 7454

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

Syntax hints:   → wi 4   = wceq 1540  ‘cfv 6561  (class class class)co 7431

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434

This theorem is referenced by:  coof  7721  eluzaddOLD  12913  eluzsubOLD  12914  fldiv4p1lem1div2  13875  fldiv4lem1div2  13877  modval  13911  seqval  14053  seqp1  14057  seqshft2  14069  monoord  14073  monoord2  14074  seqhomo  14090  facp1  14317  faclbnd4lem2  14333  bcval  14343  lsw0  14603  ccatval1  14615  ccatval2  14616  ccatalpha  14631  swrdfv  14686  2swrd2eqwrdeq  14992  imval  15146  recan  15375  rlimcld2  15614  rlimcn1  15624  rlimcn3  15626  climcn1  15628  climcn2  15629  subcn2  15631  o1of2  15649  isercoll2  15705  climsup  15706  serf0  15717  iseraltlem2  15719  fsumrelem  15843  mertenslem1  15920  mertenslem2  15921  mertens  15922  bitsfval  16460  smuval  16518  pcfac  16937  vdwlem6  17024  vdwlem8  17026  vdwlem9  17027  vdwlem10  17028  imasaddvallem  17574  imasvscafn  17582  imasvscaval  17583  mgmhmlin  18712  mhmlin  18806  mhmlem  19080  mulginvcom  19117  mhmmulg  19133  ghmlin  19239  efgsdm  19748  efgsdmi  19750  efgsrel  19752  efgsp1  19755  frgpup1  19793  rnghmmul  20449  c0snmgmhm  20462  zrrnghm  20536  abvmul  20822  abvtri  20823  issrngd  20856  lmhmlin  21034  ipcj  21652  psrmulval  21964  mhpmulcl  22153  psdcoef  22164  psdadd  22167  psdpw  22174  coe1mul2  22272  coe1tmmul2fv  22281  coe1pwmulfv  22283  cply1mul  22300  mat1scmat  22545  mdetmul  22629  madufval  22643  cramer0  22696  cpmatmcllem  22724  d1mat2pmat  22745  m2cpminvid2lem  22760  decpmatmullem  22777  decpmatmulsumfsupp  22779  pm2mpmhmlem1  22824  pm2mpmhmlem2  22825  cayhamlem1  22872  cpmadumatpoly  22889  cayleyhamilton  22896  1stcelcls  23469  imasdsf1olem  24383  comet  24526  nrmmetd  24587  tngngp  24675  tngngp3  24677  nmvs  24697  mulc1cncf  24931  cncfco  24933  pi1xfr  25088  pi1coghm  25094  caubl  25342  caublcls  25343  bcthlem2  25359  bcthlem3  25360  bcthlem4  25361  bcthlem5  25362  ivthlem2  25487  ovolicc2lem4  25555  volsuplem  25590  volsup  25591  uniioombllem3  25620  itg1climres  25749  itg2monolem1  25785  itg2i1fseqle  25789  itg2i1fseq  25790  itg2i1fseq2  25791  itg2addlem  25793  itgeq2  25813  dvferm1lem  26022  dvferm2lem  26024  dvlip  26032  c1lip1  26036  lhop1lem  26052  lhop1  26053  ftc1lem4  26080  ftc1lem6  26082  mdegmullem  26117  coe1mul3  26138  ply1divex  26176  coeeu  26264  coeeq  26266  coemullem  26289  coemul  26291  dvply1  26325  dvply2g  26326  dvply2gOLD  26327  aalioulem3  26376  aaliou3lem8  26387  ulmshftlem  26432  ulmshft  26433  ulmss  26440  pserdvlem2  26472  cxpcn3lem  26790  loglesqrt  26804  birthdaylem2  26995  emcllem2  27040  emcllem3  27041  harmonicbnd2  27048  lgamgulmlem2  27073  lgamgulmlem3  27074  lgamgulmlem5  27076  lgambdd  27080  lgamcvglem  27083  facgam  27109  ftalem7  27122  bposlem7  27334  bposlem9  27336  lgsqrlem2  27391  lgsqrlem4  27393  2lgslem3a  27440  2lgslem3b  27441  2lgslem3c  27442  2lgslem3d  27443  rplogsumlem1  27528  dchrvmasumlem1  27539  logsqvma  27586  logsqvma2  27587  selberglem3  27591  selberg  27592  selberg2lem  27594  selberg4lem1  27604  pntrsumo1  27609  selberg34r  27615  pntsval  27616  pntsval2  27620  pntrlog2bndlem1  27621  pntrlog2bndlem4  27624  pntpbnd  27632  pntibnd  27637  pntlemo  27651  addsbday  28050  seqsval  28294  seqsp1  28317  zs12bday  28424  ewlkinedg  29622  wkslem1  29625  uspgr2wlkeq  29664  wlkdlem2  29701  upgrwlkdvdelem  29756  crctcshwlkn0lem2  29831  crctcshwlkn0lem3  29832  crctcshwlkn0lem4  29833  crctcshwlkn0lem5  29834  wlkiswwlks2lem2  29890  wlkiswwlks2lem5  29893  wwlksnext  29913  wwlksnredwwlkn  29915  wwlksnextproplem2  29930  clwwlkccatlem  30008  clwlkclwwlklem2a1  30011  clwlkclwwlklem2fv1  30014  clwlkclwwlklem2a4  30016  clwlkclwwlklem2a  30017  clwlkclwwlklem2  30019  clwwisshclwwslemlem  30032  clwwisshclwws  30034  clwwlknlbonbgr1  30058  clwwlkel  30065  clwwlkf  30066  clwwlkwwlksb  30073  clwwlkext2edg  30075  wwlksext2clwwlk  30076  clwwlknonex2lem2  30127  eupthseg  30225  upgreupthseg  30228  eupth2lem3  30255  2clwwlk2clwwlklem  30365  2clwwlk  30366  numclwwlk1lem2f1  30376  numclwlk1lem2  30389  nvs  30682  nvtri  30689  ipval  30722  blocnilem  30823  phpar2  30842  phpar  30843  sii  30873  normsub0  31155  norm-ii  31157  norm-iii  31159  normsub  31162  normpyth  31164  norm3dif  31169  norm3lemt  31171  norm3adifi  31172  normpar  31174  polid  31178  bcs  31200  pjaddi  31705  pjsubi  31707  pjmuli  31708  pjcjt2  31711  lnopeq0lem2  32025  lnopunilem2  32030  branmfn  32124  hstel2  32238  stj  32254  cdj3lem1  32453  cdj3lem2b  32456  cdj3lem3b  32459  cdj3i  32460  ccatws1f1o  32936  chnltm1  32998  chnind  33001  elrgspnlem2  33247  constrsuc  33779  cnre2csqlem  33909  cnre2csqima  33910  mndpluscn  33925  lmdvg  33952  plymulx  34563  signsvfn  34597  subfacval2  35192  cvmliftlem7  35296  elmrsubrn  35525  faclim2  35748  fwddifval  36163  fwddifnval  36164  dnival  36472  unblimceq0lem  36507  unbdqndv2  36512  matunitlindf  37625  poimirlem32  37659  itg2gt0cn  37682  ftc1cnnclem  37698  ftc1cnnc  37699  areacirc  37720  sdclem1  37750  fdc  37752  seqpo  37754  incsequz  37755  incsequz2  37756  mettrifi  37764  caushft  37768  bfplem1  37829  ghomco  37898  rngohomadd  37976  rngohommul  37977  dihval  41234  lclkrlem1  41508  hdmap14lem2a  41869  hgmapval  41889  deg1pow  42142  sticksstones10  42156  sticksstones12a  42158  abvexp  42542  fsuppind  42600  prjspnval  42626  incssnn0  42722  rencldnfilem  42831  irrapxlem5  42837  irrapxlem6  42838  pellexlem3  42842  cvgdvgrat  44332  radcnvrat  44333  hashnzfzclim  44341  binomcxplemradcnv  44371  iunincfi  45099  monoords  45309  fperiodmullem  45315  monoordxrv  45492  monoordxr  45493  monoord2xrv  45494  monoord2xr  45495  climinf  45621  climsuse  45623  climinff  45626  mullimc  45631  mullimcf  45638  idlimc  45641  limcperiod  45643  limcrecl  45644  limclner  45666  climinf2  45722  climxrrelem  45764  cnrefiisplem  45844  cnrefiisp  45845  climxlim2lem  45860  cncfshift  45889  cncfperiod  45894  fperdvper  45934  dvnmul  45958  iblspltprt  45988  itgspltprt  45994  itgiccshift  45995  itgperiod  45996  dirkerval2  46109  dirkertrigeqlem1  46113  dirkertrigeqlem2  46114  dirkertrigeqlem3  46115  dirkercncflem2  46119  dirkercncflem3  46120  fourierdlem29  46151  elaa2lem  46248  elaa2  46249  nnfoctbdj  46471  meaiuninclem  46495  meaiunincf  46498  meaiuninc3v  46499  meaiuninc3  46500  meaiininclem  46501  meaiininc  46502  smflimlem6  46791  ormkglobd  46890  natglobalincr  46892  tworepnotupword  46901  smonoord  47358  iccpartimp  47404  iccelpart  47420  icceuelpart  47423  fargshiftfv  47426  fmtnorec2  47530  bgoldbtbndlem2  47793  bgoldbtbndlem3  47794  bgoldbtbnd  47796  gpgov  48001  2ltceilhalf  48015  gpg5nbgrvtx13starlem2  48028  ply1mulgsumlem3  48305  ply1mulgsumlem4  48306  ply1mulgsum  48307  ackvalsuc1  48600