Theorem fvoveq1 7453

Description: Equality theorem for nested function and operation value. Closed form of fvoveq1d 7452. (Contributed by AV, 23-Jul-2022.)

Assertion

Ref	Expression
fvoveq1	⊢ (𝐴 = 𝐵 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶)))

Proof of Theorem fvoveq1

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	fvoveq1d 7452	1 ⊢ (𝐴 = 𝐵 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶)))

This proof depends on syntax axioms:   → wi 4   = wceq 1569  ‘cfv 6547  (class class class)co 7430

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6501  df-fv 6555  df-ov 7433

This theorem is used by:  coof  7727  fldiv4p1lem1div2  13988  fldiv4lem1div2  13990  modval  14024  seqval  14168  seqp1  14172  seqshft2  14184  monoord  14188  monoord2  14189  seqhomo  14205  facp1  14435  faclbnd4lem2  14451  bcval  14461  lsw0  14723  ccatval1  14735  ccatval2  14736  ccatalpha  14753  swrdfv  14810  2swrd2eqwrdeq  15121  imval  15289  recan  15519  rlimcld2  15760  rlimcn1  15770  rlimcn3  15772  climcn1  15774  climcn2  15775  subcn2  15777  o1of2  15795  isercoll2  15851  climsup  15852  serf0  15863  iseraltlem2  15865  fsumrelem  15989  mertenslem1  16068  mertenslem2  16069  mertens  16070  bitsfval  16608  smuval  16666  pcfac  17092  vdwlem6  17179  vdwlem8  17181  vdwlem9  17182  vdwlem10  17183  imasaddvallem  17716  imasvscafn  17724  imasvscaval  17725  chnltm1  18798  chnind  18810  mgmhmlin  18903  mhmlin  19003  mhmlem  19287  mulginvcom  19324  mhmmulg  19340  ghmlin  19450  efgsdm  19959  efgsdmi  19961  efgsrel  19963  efgsp1  19966  frgpup1  20004  rnghmmul  20694  c0snmgmhm  20707  zrrnghm  20803  abvmul  21093  abvtri  21094  issrngd  21127  lmhmlin  21325  ipcj  21955  psrmulval  22267  mhpmulcl  22485  psdcoef  22496  psdadd  22499  psdpw  22506  coe1mul2  22603  coe1tmmul2fv  22612  coe1pwmulfv  22614  cply1mul  22629  mat1scmat  22869  mdetmul  22953  madufval  22967  matunitlindf  23011  cramer0  23023  cpmatmcllem  23051  d1mat2pmat  23072  m2cpminvid2lem  23087  decpmatmullem  23104  decpmatmulsumfsupp  23106  pm2mpmhmlem1  23151  pm2mpmhmlem2  23152  cayhamlem1  23199  cpmadumatpoly  23216  cayleyhamilton  23223  1stcelcls  23795  imasdsf1olem  24707  comet  24847  nrmmetd  24908  tngngp  24988  tngngp3  24990  nmvs  25010  mulc1cncf  25241  cncfco  25243  pi1xfr  25391  pi1coghm  25397  caubl  25644  caublcls  25645  bcthlem2  25661  bcthlem3  25662  bcthlem4  25663  bcthlem5  25664  ivthlem2  25788  ovolicc2lem4  25856  volsuplem  25891  volsup  25892  uniioombllem3  25921  itg1climres  26050  itg2monolem1  26086  itg2i1fseqle  26090  itg2i1fseq  26091  itg2i1fseq2  26092  itg2addlem  26094  itgeq2  26113  dvferm1lem  26319  dvferm2lem  26321  dvlip  26328  c1lip1  26332  lhop1lem  26348  lhop1  26349  ftc1lem4  26374  ftc1lem6  26376  mdegmullem  26411  coe1mul3  26432  ply1divex  26470  coeeu  26559  coeeq  26561  coemullem  26584  coemul  26586  plymulidp  26618  dvply1  26620  dvply2g  26621  aalioulem3  26676  aaliou3lem8  26687  ulmshftlem  26731  ulmshft  26732  ulmss  26739  pserdvlem2  26770  cxpcn3lem  27090  loglesqrt  27104  birthdaylem2  27295  emcllem2  27339  emcllem3  27340  harmonicbnd2  27347  lgamgulmlem2  27372  lgamgulmlem3  27373  lgamgulmlem5  27375  lgambdd  27379  lgamcvglem  27382  facgam  27408  ftalem7  27421  bposlem7  27632  bposlem9  27634  lgsqrlem2  27689  lgsqrlem4  27691  2lgslem3a  27738  2lgslem3b  27739  2lgslem3c  27740  2lgslem3d  27741  rplogsumlem1  27826  dchrvmasumlem1  27837  logsqvma  27884  logsqvma2  27885  selberglem3  27889  selberg  27890  selberg2lem  27892  selberg4lem1  27902  pntrsumo1  27907  selberg34r  27913  pntsval  27914  pntsval2  27918  pntrlog2bndlem1  27919  pntrlog2bndlem4  27922  pntpbnd  27930  pntibnd  27935  pntlemo  27949  addbday  28419  addonbday  28680  seqsval  28689  seqsp1  28712  bdaypw2n0bndlem  28864  ewlkinedg  30200  wkslem1  30203  uspgr2wlkeq  30241  wlkdlem2  30277  upgrwlkdvdelem  30337  crctcshwlkn0lem2  30415  crctcshwlkn0lem3  30416  crctcshwlkn0lem4  30417  crctcshwlkn0lem5  30418  wlkiswwlks2lem2  30474  wlkiswwlks2lem5  30477  wwlksnext  30497  wwlksnredwwlkn  30499  wwlksnextproplem2  30514  clwwlkccatlem  30595  clwlkclwwlklem2a1  30598  clwlkclwwlklem2fv1  30601  clwlkclwwlklem2a4  30603  clwlkclwwlklem2a  30604  clwlkclwwlklem2  30606  clwwisshclwwslemlem  30619  clwwisshclwws  30621  clwwlknlbonbgr1  30645  clwwlkel  30652  clwwlkf  30653  clwwlkwwlksb  30660  clwwlkext2edg  30662  wwlksext2clwwlk  30663  clwwlknonex2lem2  30714  eupthseg  30822  upgreupthseg  30825  eupth2lem3  30852  2clwwlk2clwwlklem  30962  2clwwlk  30963  numclwwlk1lem2f1  30973  numclwlk1lem2  30986  nvs  31280  nvtri  31287  ipval  31320  blocnilem  31421  phpar2  31440  phpar  31441  sii  31471  normsub0  31753  norm-ii  31755  norm-iii  31757  normsub  31760  normpyth  31762  norm3dif  31767  norm3lemt  31769  norm3adifi  31770  normpar  31772  polid  31776  bcs  31798  pjaddi  32303  pjsubi  32305  pjmuli  32306  pjcjt2  32309  lnopeq0lem2  32623  lnopunilem2  32628  branmfn  32722  hstel2  32836  stj  32852  cdj3lem1  33051  cdj3lem2b  33054  cdj3lem3b  33057  cdj3i  33058  ccatws1f1o  33570  gsummulsubdishift1  33685  elrgspnlem2  33860  selvply1rhmlemb  34207  constrsuc  34426  cnre2csqlem  34598  cnre2csqima  34599  mndpluscn  34614  lmdvg  34641  signsvfn  35267  subfacval2  36076  cvmliftlem7  36180  elmrsubrn  36409  faclim2  36643  fwddifval  37057  fwddifnval  37058  dnival  37467  unblimceq0lem  37502  unbdqndv2  37507  poimirlem32  38713  itg2gt0cn  38736  ftc1cnnclem  38752  ftc1cnnc  38753  areacirc  38774  sdclem1  38820  fdc  38822  seqpo  38824  incsequz  38825  incsequz2  38826  mettrifi  38834  caushft  38838  bfplem1  38899  ghomco  38968  rngohomadd  39046  rngohommul  39047  dihval  42432  lclkrlem1  42706  hdmap14lem2a  43067  hgmapval  43087  deg1pow  43334  sticksstones10  43348  sticksstones12a  43350  abvexp  43739  fsuppind  43761  prjspnval  43787  incssnn0  43865  rencldnfilem  43970  irrapxlem5  43976  irrapxlem6  43977  pellexlem3  43981  cvgdvgrat  45440  radcnvrat  45441  hashnzfzclim  45449  binomcxplemradcnv  45479  iunincfi  46251  monoords  46455  fperiodmullem  46461  monoordxrv  46633  monoordxr  46634  monoord2xrv  46635  monoord2xr  46636  climinf  46760  climsuse  46762  climinff  46765  mullimc  46770  mullimcf  46777  idlimc  46780  limcperiod  46782  limcrecl  46783  limclner  46803  climinf2  46859  climxrrelem  46901  cnrefiisplem  46981  cnrefiisp  46982  climxlim2lem  46997  cncfshift  47026  cncfperiod  47031  fperdvper  47071  dvnmul  47095  iblspltprt  47125  itgspltprt  47131  itgiccshift  47132  itgperiod  47133  dirkerval2  47246  dirkertrigeqlem1  47250  dirkertrigeqlem2  47251  dirkertrigeqlem3  47252  dirkercncflem2  47256  dirkercncflem3  47257  fourierdlem29  47288  fourierdlem48  47306  fourierdlem49  47307  fourierdlem113  47371  elaa2lem  47385  elaa2  47386  nnfoctbdj  47608  meaiuninclem  47632  meaiunincf  47635  meaiuninc3v  47636  meaiuninc3  47637  meaiininclem  47638  meaiininc  47639  smflimlem6  47928  ormkglobd  48029  2ltceilhalf  48544  ceilhalfnn  48552  smonoord  48589  iccpartimp  48641  iccelpart  48657  icceuelpart  48660  fargshiftfv  48663  fmtnorec2  48770  ppivalnnnprmge6  48853  ppivalnnnprm  48855  ppivalnn  48859  bgoldbtbndlem2  49046  bgoldbtbndlem3  49047  bgoldbtbnd  49049  upgrimwlklem5  49141  gpgov  49282  gpg5nbgrvtx13starlem2  49312  ply1mulgsumlem3  49642  ply1mulgsumlem4  49643  ply1mulgsum  49644  ackvalsuc1  49933