Theorem fvoveq1 7392

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

Syntax hints:   → wi 4   = wceq 1540  ‘cfv 6499  (class class class)co 7369

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372

This theorem is referenced by:  coof  7657  eluzaddOLD  12804  eluzsubOLD  12805  fldiv4p1lem1div2  13773  fldiv4lem1div2  13775  modval  13809  seqval  13953  seqp1  13957  seqshft2  13969  monoord  13973  monoord2  13974  seqhomo  13990  facp1  14219  faclbnd4lem2  14235  bcval  14245  lsw0  14506  ccatval1  14518  ccatval2  14519  ccatalpha  14534  swrdfv  14589  2swrd2eqwrdeq  14895  imval  15049  recan  15279  rlimcld2  15520  rlimcn1  15530  rlimcn3  15532  climcn1  15534  climcn2  15535  subcn2  15537  o1of2  15555  isercoll2  15611  climsup  15612  serf0  15623  iseraltlem2  15625  fsumrelem  15749  mertenslem1  15826  mertenslem2  15827  mertens  15828  bitsfval  16369  smuval  16427  pcfac  16846  vdwlem6  16933  vdwlem8  16935  vdwlem9  16936  vdwlem10  16937  imasaddvallem  17468  imasvscafn  17476  imasvscaval  17477  mgmhmlin  18608  mhmlin  18702  mhmlem  18976  mulginvcom  19013  mhmmulg  19029  ghmlin  19135  efgsdm  19644  efgsdmi  19646  efgsrel  19648  efgsp1  19651  frgpup1  19689  rnghmmul  20369  c0snmgmhm  20382  zrrnghm  20456  abvmul  20741  abvtri  20742  issrngd  20775  lmhmlin  20974  ipcj  21576  psrmulval  21886  mhpmulcl  22069  psdcoef  22080  psdadd  22083  psdpw  22090  coe1mul2  22188  coe1tmmul2fv  22197  coe1pwmulfv  22199  cply1mul  22216  mat1scmat  22459  mdetmul  22543  madufval  22557  cramer0  22610  cpmatmcllem  22638  d1mat2pmat  22659  m2cpminvid2lem  22674  decpmatmullem  22691  decpmatmulsumfsupp  22693  pm2mpmhmlem1  22738  pm2mpmhmlem2  22739  cayhamlem1  22786  cpmadumatpoly  22803  cayleyhamilton  22810  1stcelcls  23381  imasdsf1olem  24294  comet  24434  nrmmetd  24495  tngngp  24575  tngngp3  24577  nmvs  24597  mulc1cncf  24831  cncfco  24833  pi1xfr  24988  pi1coghm  24994  caubl  25241  caublcls  25242  bcthlem2  25258  bcthlem3  25259  bcthlem4  25260  bcthlem5  25261  ivthlem2  25386  ovolicc2lem4  25454  volsuplem  25489  volsup  25490  uniioombllem3  25519  itg1climres  25648  itg2monolem1  25684  itg2i1fseqle  25688  itg2i1fseq  25689  itg2i1fseq2  25690  itg2addlem  25692  itgeq2  25712  dvferm1lem  25921  dvferm2lem  25923  dvlip  25931  c1lip1  25935  lhop1lem  25951  lhop1  25952  ftc1lem4  25979  ftc1lem6  25981  mdegmullem  26016  coe1mul3  26037  ply1divex  26075  coeeu  26163  coeeq  26165  coemullem  26188  coemul  26190  dvply1  26224  dvply2g  26225  dvply2gOLD  26226  aalioulem3  26275  aaliou3lem8  26286  ulmshftlem  26331  ulmshft  26332  ulmss  26339  pserdvlem2  26371  cxpcn3lem  26690  loglesqrt  26704  birthdaylem2  26895  emcllem2  26940  emcllem3  26941  harmonicbnd2  26948  lgamgulmlem2  26973  lgamgulmlem3  26974  lgamgulmlem5  26976  lgambdd  26980  lgamcvglem  26983  facgam  27009  ftalem7  27022  bposlem7  27234  bposlem9  27236  lgsqrlem2  27291  lgsqrlem4  27293  2lgslem3a  27340  2lgslem3b  27341  2lgslem3c  27342  2lgslem3d  27343  rplogsumlem1  27428  dchrvmasumlem1  27439  logsqvma  27486  logsqvma2  27487  selberglem3  27491  selberg  27492  selberg2lem  27494  selberg4lem1  27504  pntrsumo1  27509  selberg34r  27515  pntsval  27516  pntsval2  27520  pntrlog2bndlem1  27521  pntrlog2bndlem4  27524  pntpbnd  27532  pntibnd  27537  pntlemo  27551  addsbday  27964  seqsval  28222  seqsp1  28245  zs12bday  28396  ewlkinedg  29585  wkslem1  29588  uspgr2wlkeq  29626  wlkdlem2  29662  upgrwlkdvdelem  29716  crctcshwlkn0lem2  29791  crctcshwlkn0lem3  29792  crctcshwlkn0lem4  29793  crctcshwlkn0lem5  29794  wlkiswwlks2lem2  29850  wlkiswwlks2lem5  29853  wwlksnext  29873  wwlksnredwwlkn  29875  wwlksnextproplem2  29890  clwwlkccatlem  29968  clwlkclwwlklem2a1  29971  clwlkclwwlklem2fv1  29974  clwlkclwwlklem2a4  29976  clwlkclwwlklem2a  29977  clwlkclwwlklem2  29979  clwwisshclwwslemlem  29992  clwwisshclwws  29994  clwwlknlbonbgr1  30018  clwwlkel  30025  clwwlkf  30026  clwwlkwwlksb  30033  clwwlkext2edg  30035  wwlksext2clwwlk  30036  clwwlknonex2lem2  30087  eupthseg  30185  upgreupthseg  30188  eupth2lem3  30215  2clwwlk2clwwlklem  30325  2clwwlk  30326  numclwwlk1lem2f1  30336  numclwlk1lem2  30349  nvs  30642  nvtri  30649  ipval  30682  blocnilem  30783  phpar2  30802  phpar  30803  sii  30833  normsub0  31115  norm-ii  31117  norm-iii  31119  normsub  31122  normpyth  31124  norm3dif  31129  norm3lemt  31131  norm3adifi  31132  normpar  31134  polid  31138  bcs  31160  pjaddi  31665  pjsubi  31667  pjmuli  31668  pjcjt2  31671  lnopeq0lem2  31985  lnopunilem2  31990  branmfn  32084  hstel2  32198  stj  32214  cdj3lem1  32413  cdj3lem2b  32416  cdj3lem3b  32419  cdj3i  32420  ccatws1f1o  32923  chnltm1  32980  chnind  32983  elrgspnlem2  33210  constrsuc  33721  cnre2csqlem  33893  cnre2csqima  33894  mndpluscn  33909  lmdvg  33936  plymulx  34532  signsvfn  34566  subfacval2  35167  cvmliftlem7  35271  elmrsubrn  35500  faclim2  35728  fwddifval  36143  fwddifnval  36144  dnival  36452  unblimceq0lem  36487  unbdqndv2  36492  matunitlindf  37605  poimirlem32  37639  itg2gt0cn  37662  ftc1cnnclem  37678  ftc1cnnc  37679  areacirc  37700  sdclem1  37730  fdc  37732  seqpo  37734  incsequz  37735  incsequz2  37736  mettrifi  37744  caushft  37748  bfplem1  37809  ghomco  37878  rngohomadd  37956  rngohommul  37957  dihval  41219  lclkrlem1  41493  hdmap14lem2a  41854  hgmapval  41874  deg1pow  42122  sticksstones10  42136  sticksstones12a  42138  abvexp  42513  fsuppind  42571  prjspnval  42597  incssnn0  42692  rencldnfilem  42801  irrapxlem5  42807  irrapxlem6  42808  pellexlem3  42812  cvgdvgrat  44295  radcnvrat  44296  hashnzfzclim  44304  binomcxplemradcnv  44334  iunincfi  45081  monoords  45288  fperiodmullem  45294  monoordxrv  45470  monoordxr  45471  monoord2xrv  45472  monoord2xr  45473  climinf  45597  climsuse  45599  climinff  45602  mullimc  45607  mullimcf  45614  idlimc  45617  limcperiod  45619  limcrecl  45620  limclner  45642  climinf2  45698  climxrrelem  45740  cnrefiisplem  45820  cnrefiisp  45821  climxlim2lem  45836  cncfshift  45865  cncfperiod  45870  fperdvper  45910  dvnmul  45934  iblspltprt  45964  itgspltprt  45970  itgiccshift  45971  itgperiod  45972  dirkerval2  46085  dirkertrigeqlem1  46089  dirkertrigeqlem2  46090  dirkertrigeqlem3  46091  dirkercncflem2  46095  dirkercncflem3  46096  fourierdlem29  46127  elaa2lem  46224  elaa2  46225  nnfoctbdj  46447  meaiuninclem  46471  meaiunincf  46474  meaiuninc3v  46475  meaiuninc3  46476  meaiininclem  46477  meaiininc  46478  smflimlem6  46767  ormkglobd  46866  natglobalincr  46868  tworepnotupword  46877  2ltceilhalf  47322  ceilhalfnn  47330  smonoord  47365  iccpartimp  47411  iccelpart  47427  icceuelpart  47430  fargshiftfv  47433  fmtnorec2  47537  bgoldbtbndlem2  47800  bgoldbtbndlem3  47801  bgoldbtbnd  47803  upgrimwlklem5  47894  gpgov  48026  gpg5nbgrvtx13starlem2  48056  ply1mulgsumlem3  48370  ply1mulgsumlem4  48371  ply1mulgsum  48372  ackvalsuc1  48661