Theorem fvoveq1 7471

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

Syntax hints:   → wi 4   = wceq 1537  ‘cfv 6573  (class class class)co 7448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451

This theorem is referenced by:  coof  7737  eluzaddOLD  12938  eluzsubOLD  12939  fldiv4p1lem1div2  13886  fldiv4lem1div2  13888  modval  13922  seqval  14063  seqp1  14067  seqshft2  14079  monoord  14083  monoord2  14084  seqhomo  14100  facp1  14327  faclbnd4lem2  14343  bcval  14353  lsw0  14613  ccatval1  14625  ccatval2  14626  ccatalpha  14641  swrdfv  14696  2swrd2eqwrdeq  15002  imval  15156  recan  15385  rlimcld2  15624  rlimcn1  15634  rlimcn3  15636  climcn1  15638  climcn2  15639  subcn2  15641  o1of2  15659  isercoll2  15717  climsup  15718  serf0  15729  iseraltlem2  15731  fsumrelem  15855  mertenslem1  15932  mertenslem2  15933  mertens  15934  bitsfval  16469  smuval  16527  pcfac  16946  vdwlem6  17033  vdwlem8  17035  vdwlem9  17036  vdwlem10  17037  imasaddvallem  17589  imasvscafn  17597  imasvscaval  17598  mgmhmlin  18737  mhmlin  18828  mhmlem  19102  mulginvcom  19139  mhmmulg  19155  ghmlin  19261  efgsdm  19772  efgsdmi  19774  efgsrel  19776  efgsp1  19779  frgpup1  19817  rnghmmul  20475  c0snmgmhm  20488  zrrnghm  20562  abvmul  20844  abvtri  20845  issrngd  20878  lmhmlin  21057  ipcj  21675  psrmulval  21987  mhpmulcl  22176  psdcoef  22187  psdadd  22190  coe1mul2  22293  coe1tmmul2fv  22302  coe1pwmulfv  22304  cply1mul  22321  mat1scmat  22566  mdetmul  22650  madufval  22664  cramer0  22717  cpmatmcllem  22745  d1mat2pmat  22766  m2cpminvid2lem  22781  decpmatmullem  22798  decpmatmulsumfsupp  22800  pm2mpmhmlem1  22845  pm2mpmhmlem2  22846  cayhamlem1  22893  cpmadumatpoly  22910  cayleyhamilton  22917  1stcelcls  23490  imasdsf1olem  24404  comet  24547  nrmmetd  24608  tngngp  24696  tngngp3  24698  nmvs  24718  mulc1cncf  24950  cncfco  24952  pi1xfr  25107  pi1coghm  25113  caubl  25361  caublcls  25362  bcthlem2  25378  bcthlem3  25379  bcthlem4  25380  bcthlem5  25381  ivthlem2  25506  ovolicc2lem4  25574  volsuplem  25609  volsup  25610  uniioombllem3  25639  itg1climres  25769  itg2monolem1  25805  itg2i1fseqle  25809  itg2i1fseq  25810  itg2i1fseq2  25811  itg2addlem  25813  itgeq2  25833  dvferm1lem  26042  dvferm2lem  26044  dvlip  26052  c1lip1  26056  lhop1lem  26072  lhop1  26073  ftc1lem4  26100  ftc1lem6  26102  mdegmullem  26137  coe1mul3  26158  ply1divex  26196  coeeu  26284  coeeq  26286  coemullem  26309  coemul  26311  dvply1  26343  dvply2g  26344  dvply2gOLD  26345  aalioulem3  26394  aaliou3lem8  26405  ulmshftlem  26450  ulmshft  26451  ulmss  26458  pserdvlem2  26490  cxpcn3lem  26808  loglesqrt  26822  birthdaylem2  27013  emcllem2  27058  emcllem3  27059  harmonicbnd2  27066  lgamgulmlem2  27091  lgamgulmlem3  27092  lgamgulmlem5  27094  lgambdd  27098  lgamcvglem  27101  facgam  27127  ftalem7  27140  bposlem7  27352  bposlem9  27354  lgsqrlem2  27409  lgsqrlem4  27411  2lgslem3a  27458  2lgslem3b  27459  2lgslem3c  27460  2lgslem3d  27461  rplogsumlem1  27546  dchrvmasumlem1  27557  logsqvma  27604  logsqvma2  27605  selberglem3  27609  selberg  27610  selberg2lem  27612  selberg4lem1  27622  pntrsumo1  27627  selberg34r  27633  pntsval  27634  pntsval2  27638  pntrlog2bndlem1  27639  pntrlog2bndlem4  27642  pntpbnd  27650  pntibnd  27655  pntlemo  27669  addsbday  28068  seqsval  28312  seqsp1  28335  zs12bday  28442  ewlkinedg  29640  wkslem1  29643  uspgr2wlkeq  29682  wlkdlem2  29719  upgrwlkdvdelem  29772  crctcshwlkn0lem2  29844  crctcshwlkn0lem3  29845  crctcshwlkn0lem4  29846  crctcshwlkn0lem5  29847  wlkiswwlks2lem2  29903  wlkiswwlks2lem5  29906  wwlksnext  29926  wwlksnredwwlkn  29928  wwlksnextproplem2  29943  clwwlkccatlem  30021  clwlkclwwlklem2a1  30024  clwlkclwwlklem2fv1  30027  clwlkclwwlklem2a4  30029  clwlkclwwlklem2a  30030  clwlkclwwlklem2  30032  clwwisshclwwslemlem  30045  clwwisshclwws  30047  clwwlknlbonbgr1  30071  clwwlkel  30078  clwwlkf  30079  clwwlkwwlksb  30086  clwwlkext2edg  30088  wwlksext2clwwlk  30089  clwwlknonex2lem2  30140  eupthseg  30238  upgreupthseg  30241  eupth2lem3  30268  2clwwlk2clwwlklem  30378  2clwwlk  30379  numclwwlk1lem2f1  30389  numclwlk1lem2  30402  nvs  30695  nvtri  30702  ipval  30735  blocnilem  30836  phpar2  30855  phpar  30856  sii  30886  normsub0  31168  norm-ii  31170  norm-iii  31172  normsub  31175  normpyth  31177  norm3dif  31182  norm3lemt  31184  norm3adifi  31185  normpar  31187  polid  31191  bcs  31213  pjaddi  31718  pjsubi  31720  pjmuli  31721  pjcjt2  31724  lnopeq0lem2  32038  lnopunilem2  32043  branmfn  32137  hstel2  32251  stj  32267  cdj3lem1  32466  cdj3lem2b  32469  cdj3lem3b  32472  cdj3i  32473  ccatws1f1o  32918  chnltm1  32981  chnind  32983  constrsuc  33728  cnre2csqlem  33856  cnre2csqima  33857  mndpluscn  33872  lmdvg  33899  plymulx  34525  signsvfn  34559  subfacval2  35155  cvmliftlem7  35259  elmrsubrn  35488  faclim2  35710  fwddifval  36126  fwddifnval  36127  dnival  36437  unblimceq0lem  36472  unbdqndv2  36477  matunitlindf  37578  poimirlem32  37612  itg2gt0cn  37635  ftc1cnnclem  37651  ftc1cnnc  37652  areacirc  37673  sdclem1  37703  fdc  37705  seqpo  37707  incsequz  37708  incsequz2  37709  mettrifi  37717  caushft  37721  bfplem1  37782  ghomco  37851  rngohomadd  37929  rngohommul  37930  dihval  41189  lclkrlem1  41463  hdmap14lem2a  41824  hgmapval  41844  deg1pow  42098  sticksstones10  42112  sticksstones12a  42114  abvexp  42487  fsuppind  42545  prjspnval  42571  incssnn0  42667  rencldnfilem  42776  irrapxlem5  42782  irrapxlem6  42783  pellexlem3  42787  cvgdvgrat  44282  radcnvrat  44283  hashnzfzclim  44291  binomcxplemradcnv  44321  iunincfi  44996  monoords  45212  fperiodmullem  45218  monoordxrv  45397  monoordxr  45398  monoord2xrv  45399  monoord2xr  45400  climinf  45527  climsuse  45529  climinff  45532  mullimc  45537  mullimcf  45544  idlimc  45547  limcperiod  45549  limcrecl  45550  limclner  45572  climinf2  45628  climxrrelem  45670  cnrefiisplem  45750  cnrefiisp  45751  climxlim2lem  45766  cncfshift  45795  cncfperiod  45800  fperdvper  45840  dvnmul  45864  iblspltprt  45894  itgspltprt  45900  itgiccshift  45901  itgperiod  45902  dirkerval2  46015  dirkertrigeqlem1  46019  dirkertrigeqlem2  46020  dirkertrigeqlem3  46021  dirkercncflem2  46025  dirkercncflem3  46026  fourierdlem29  46057  elaa2lem  46154  elaa2  46155  nnfoctbdj  46377  meaiuninclem  46401  meaiunincf  46404  meaiuninc3v  46405  meaiuninc3  46406  meaiininclem  46407  meaiininc  46408  smflimlem6  46697  natglobalincr  46796  tworepnotupword  46805  smonoord  47245  iccpartimp  47291  iccelpart  47307  icceuelpart  47310  fargshiftfv  47313  fmtnorec2  47417  bgoldbtbndlem2  47680  bgoldbtbndlem3  47681  bgoldbtbnd  47683  ply1mulgsumlem3  48117  ply1mulgsumlem4  48118  ply1mulgsum  48119  ackvalsuc1  48413