Theorem fvoveq1 7369

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

Syntax hints:   → wi 4   = wceq 1541  ‘cfv 6481  (class class class)co 7346

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489  df-ov 7349

This theorem is referenced by:  coof  7634  eluzaddOLD  12767  eluzsubOLD  12768  fldiv4p1lem1div2  13739  fldiv4lem1div2  13741  modval  13775  seqval  13919  seqp1  13923  seqshft2  13935  monoord  13939  monoord2  13940  seqhomo  13956  facp1  14185  faclbnd4lem2  14201  bcval  14211  lsw0  14472  ccatval1  14484  ccatval2  14485  ccatalpha  14501  swrdfv  14556  2swrd2eqwrdeq  14860  imval  15014  recan  15244  rlimcld2  15485  rlimcn1  15495  rlimcn3  15497  climcn1  15499  climcn2  15500  subcn2  15502  o1of2  15520  isercoll2  15576  climsup  15577  serf0  15588  iseraltlem2  15590  fsumrelem  15714  mertenslem1  15791  mertenslem2  15792  mertens  15793  bitsfval  16334  smuval  16392  pcfac  16811  vdwlem6  16898  vdwlem8  16900  vdwlem9  16901  vdwlem10  16902  imasaddvallem  17433  imasvscafn  17441  imasvscaval  17442  chnltm1  18515  chnind  18527  mgmhmlin  18607  mhmlin  18701  mhmlem  18975  mulginvcom  19012  mhmmulg  19028  ghmlin  19133  efgsdm  19642  efgsdmi  19644  efgsrel  19646  efgsp1  19649  frgpup1  19687  rnghmmul  20367  c0snmgmhm  20380  zrrnghm  20451  abvmul  20736  abvtri  20737  issrngd  20770  lmhmlin  20969  ipcj  21571  psrmulval  21881  mhpmulcl  22064  psdcoef  22075  psdadd  22078  psdpw  22085  coe1mul2  22183  coe1tmmul2fv  22192  coe1pwmulfv  22194  cply1mul  22211  mat1scmat  22454  mdetmul  22538  madufval  22552  cramer0  22605  cpmatmcllem  22633  d1mat2pmat  22654  m2cpminvid2lem  22669  decpmatmullem  22686  decpmatmulsumfsupp  22688  pm2mpmhmlem1  22733  pm2mpmhmlem2  22734  cayhamlem1  22781  cpmadumatpoly  22798  cayleyhamilton  22805  1stcelcls  23376  imasdsf1olem  24288  comet  24428  nrmmetd  24489  tngngp  24569  tngngp3  24571  nmvs  24591  mulc1cncf  24825  cncfco  24827  pi1xfr  24982  pi1coghm  24988  caubl  25235  caublcls  25236  bcthlem2  25252  bcthlem3  25253  bcthlem4  25254  bcthlem5  25255  ivthlem2  25380  ovolicc2lem4  25448  volsuplem  25483  volsup  25484  uniioombllem3  25513  itg1climres  25642  itg2monolem1  25678  itg2i1fseqle  25682  itg2i1fseq  25683  itg2i1fseq2  25684  itg2addlem  25686  itgeq2  25706  dvferm1lem  25915  dvferm2lem  25917  dvlip  25925  c1lip1  25929  lhop1lem  25945  lhop1  25946  ftc1lem4  25973  ftc1lem6  25975  mdegmullem  26010  coe1mul3  26031  ply1divex  26069  coeeu  26157  coeeq  26159  coemullem  26182  coemul  26184  dvply1  26218  dvply2g  26219  dvply2gOLD  26220  aalioulem3  26269  aaliou3lem8  26280  ulmshftlem  26325  ulmshft  26326  ulmss  26333  pserdvlem2  26365  cxpcn3lem  26684  loglesqrt  26698  birthdaylem2  26889  emcllem2  26934  emcllem3  26935  harmonicbnd2  26942  lgamgulmlem2  26967  lgamgulmlem3  26968  lgamgulmlem5  26970  lgambdd  26974  lgamcvglem  26977  facgam  27003  ftalem7  27016  bposlem7  27228  bposlem9  27230  lgsqrlem2  27285  lgsqrlem4  27287  2lgslem3a  27334  2lgslem3b  27335  2lgslem3c  27336  2lgslem3d  27337  rplogsumlem1  27422  dchrvmasumlem1  27433  logsqvma  27480  logsqvma2  27481  selberglem3  27485  selberg  27486  selberg2lem  27488  selberg4lem1  27498  pntrsumo1  27503  selberg34r  27509  pntsval  27510  pntsval2  27514  pntrlog2bndlem1  27515  pntrlog2bndlem4  27518  pntpbnd  27526  pntibnd  27531  pntlemo  27545  addsbday  27960  seqsval  28218  seqsp1  28241  zs12bday  28394  ewlkinedg  29583  wkslem1  29586  uspgr2wlkeq  29624  wlkdlem2  29660  upgrwlkdvdelem  29714  crctcshwlkn0lem2  29789  crctcshwlkn0lem3  29790  crctcshwlkn0lem4  29791  crctcshwlkn0lem5  29792  wlkiswwlks2lem2  29848  wlkiswwlks2lem5  29851  wwlksnext  29871  wwlksnredwwlkn  29873  wwlksnextproplem2  29888  clwwlkccatlem  29969  clwlkclwwlklem2a1  29972  clwlkclwwlklem2fv1  29975  clwlkclwwlklem2a4  29977  clwlkclwwlklem2a  29978  clwlkclwwlklem2  29980  clwwisshclwwslemlem  29993  clwwisshclwws  29995  clwwlknlbonbgr1  30019  clwwlkel  30026  clwwlkf  30027  clwwlkwwlksb  30034  clwwlkext2edg  30036  wwlksext2clwwlk  30037  clwwlknonex2lem2  30088  eupthseg  30186  upgreupthseg  30189  eupth2lem3  30216  2clwwlk2clwwlklem  30326  2clwwlk  30327  numclwwlk1lem2f1  30337  numclwlk1lem2  30350  nvs  30643  nvtri  30650  ipval  30683  blocnilem  30784  phpar2  30803  phpar  30804  sii  30834  normsub0  31116  norm-ii  31118  norm-iii  31120  normsub  31123  normpyth  31125  norm3dif  31130  norm3lemt  31132  norm3adifi  31133  normpar  31135  polid  31139  bcs  31161  pjaddi  31666  pjsubi  31668  pjmuli  31669  pjcjt2  31672  lnopeq0lem2  31986  lnopunilem2  31991  branmfn  32085  hstel2  32199  stj  32215  cdj3lem1  32414  cdj3lem2b  32417  cdj3lem3b  32420  cdj3i  32421  ccatws1f1o  32932  elrgspnlem2  33210  constrsuc  33751  cnre2csqlem  33923  cnre2csqima  33924  mndpluscn  33939  lmdvg  33966  plymulx  34561  signsvfn  34595  subfacval2  35231  cvmliftlem7  35335  elmrsubrn  35564  faclim2  35792  fwddifval  36206  fwddifnval  36207  dnival  36515  unblimceq0lem  36550  unbdqndv2  36555  matunitlindf  37668  poimirlem32  37702  itg2gt0cn  37725  ftc1cnnclem  37741  ftc1cnnc  37742  areacirc  37763  sdclem1  37793  fdc  37795  seqpo  37797  incsequz  37798  incsequz2  37799  mettrifi  37807  caushft  37811  bfplem1  37872  ghomco  37941  rngohomadd  38019  rngohommul  38020  dihval  41341  lclkrlem1  41615  hdmap14lem2a  41976  hgmapval  41996  deg1pow  42244  sticksstones10  42258  sticksstones12a  42260  abvexp  42635  fsuppind  42693  prjspnval  42719  incssnn0  42814  rencldnfilem  42923  irrapxlem5  42929  irrapxlem6  42930  pellexlem3  42934  cvgdvgrat  44416  radcnvrat  44417  hashnzfzclim  44425  binomcxplemradcnv  44455  iunincfi  45201  monoords  45408  fperiodmullem  45414  monoordxrv  45589  monoordxr  45590  monoord2xrv  45591  monoord2xr  45592  climinf  45716  climsuse  45718  climinff  45721  mullimc  45726  mullimcf  45733  idlimc  45736  limcperiod  45738  limcrecl  45739  limclner  45759  climinf2  45815  climxrrelem  45857  cnrefiisplem  45937  cnrefiisp  45938  climxlim2lem  45953  cncfshift  45982  cncfperiod  45987  fperdvper  46027  dvnmul  46051  iblspltprt  46081  itgspltprt  46087  itgiccshift  46088  itgperiod  46089  dirkerval2  46202  dirkertrigeqlem1  46206  dirkertrigeqlem2  46207  dirkertrigeqlem3  46208  dirkercncflem2  46212  dirkercncflem3  46213  fourierdlem29  46244  elaa2lem  46341  elaa2  46342  nnfoctbdj  46564  meaiuninclem  46588  meaiunincf  46591  meaiuninc3v  46592  meaiuninc3  46593  meaiininclem  46594  meaiininc  46595  smflimlem6  46884  ormkglobd  46983  natglobalincr  46985  2ltceilhalf  47438  ceilhalfnn  47446  smonoord  47481  iccpartimp  47527  iccelpart  47543  icceuelpart  47546  fargshiftfv  47549  fmtnorec2  47653  bgoldbtbndlem2  47916  bgoldbtbndlem3  47917  bgoldbtbnd  47919  upgrimwlklem5  48011  gpgov  48152  gpg5nbgrvtx13starlem2  48182  ply1mulgsumlem3  48499  ply1mulgsumlem4  48500  ply1mulgsum  48501  ackvalsuc1  48790