Theorem fvoveq1 7443

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ‘cfv 6538  (class class class)co 7420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6494  df-fv 6546  df-ov 7423

This theorem is used by:  coof  7717  fldiv4p1lem1div2  13975  fldiv4lem1div2  13977  modval  14011  seqval  14155  seqp1  14159  seqshft2  14171  monoord  14175  monoord2  14176  seqhomo  14192  facp1  14422  faclbnd4lem2  14438  bcval  14448  lsw0  14710  ccatval1  14722  ccatval2  14723  ccatalpha  14740  swrdfv  14796  2swrd2eqwrdeq  15106  imval  15274  recan  15504  rlimcld2  15745  rlimcn1  15755  rlimcn3  15757  climcn1  15759  climcn2  15760  subcn2  15762  o1of2  15780  isercoll2  15836  climsup  15837  serf0  15848  iseraltlem2  15850  fsumrelem  15974  mertenslem1  16053  mertenslem2  16054  mertens  16055  bitsfval  16593  smuval  16651  pcfac  17077  vdwlem6  17164  vdwlem8  17166  vdwlem9  17167  vdwlem10  17168  imasaddvallem  17701  imasvscafn  17709  imasvscaval  17710  chnltm1  18783  chnind  18795  mgmhmlin  18888  mhmlin  18988  mhmlem  19272  mulginvcom  19309  mhmmulg  19325  ghmlin  19435  efgsdm  19944  efgsdmi  19946  efgsrel  19948  efgsp1  19951  frgpup1  19989  rnghmmul  20679  c0snmgmhm  20692  zrrnghm  20788  abvmul  21078  abvtri  21079  issrngd  21112  lmhmlin  21310  ipcj  21940  psrmulval  22252  mhpmulcl  22470  psdcoef  22481  psdadd  22484  psdpw  22491  coe1mul2  22588  coe1tmmul2fv  22597  coe1pwmulfv  22599  cply1mul  22614  mat1scmat  22854  mdetmul  22938  madufval  22952  matunitlindf  22996  cramer0  23008  cpmatmcllem  23036  d1mat2pmat  23057  m2cpminvid2lem  23072  decpmatmullem  23089  decpmatmulsumfsupp  23091  pm2mpmhmlem1  23136  pm2mpmhmlem2  23137  cayhamlem1  23184  cpmadumatpoly  23201  cayleyhamilton  23208  1stcelcls  23780  imasdsf1olem  24692  comet  24832  nrmmetd  24893  tngngp  24973  tngngp3  24975  nmvs  24995  mulc1cncf  25226  cncfco  25228  pi1xfr  25376  pi1coghm  25382  caubl  25629  caublcls  25630  bcthlem2  25646  bcthlem3  25647  bcthlem4  25648  bcthlem5  25649  ivthlem2  25773  ovolicc2lem4  25841  volsuplem  25876  volsup  25877  uniioombllem3  25906  itg1climres  26035  itg2monolem1  26071  itg2i1fseqle  26075  itg2i1fseq  26076  itg2i1fseq2  26077  itg2addlem  26079  itgeq2  26098  dvferm1lem  26304  dvferm2lem  26306  dvlip  26313  c1lip1  26317  lhop1lem  26333  lhop1  26334  ftc1lem4  26359  ftc1lem6  26361  mdegmullem  26396  coe1mul3  26417  ply1divex  26455  coeeu  26544  coeeq  26546  coemullem  26569  coemul  26571  plymulidp  26603  dvply1  26605  dvply2g  26606  aalioulem3  26661  aaliou3lem8  26672  ulmshftlem  26716  ulmshft  26717  ulmss  26724  pserdvlem2  26755  cxpcn3lem  27075  loglesqrt  27089  birthdaylem2  27280  emcllem2  27324  emcllem3  27325  harmonicbnd2  27332  lgamgulmlem2  27357  lgamgulmlem3  27358  lgamgulmlem5  27360  lgambdd  27364  lgamcvglem  27367  facgam  27393  ftalem7  27406  bposlem7  27617  bposlem9  27619  lgsqrlem2  27674  lgsqrlem4  27676  2lgslem3a  27723  2lgslem3b  27724  2lgslem3c  27725  2lgslem3d  27726  rplogsumlem1  27811  dchrvmasumlem1  27822  logsqvma  27869  logsqvma2  27870  selberglem3  27874  selberg  27875  selberg2lem  27877  selberg4lem1  27887  pntrsumo1  27892  selberg34r  27898  pntsval  27899  pntsval2  27903  pntrlog2bndlem1  27904  pntrlog2bndlem4  27907  pntpbnd  27915  pntibnd  27920  pntlemo  27934  addbday  28404  addonbday  28665  seqsval  28674  seqsp1  28697  bdaypw2n0bndlem  28849  ewlkinedg  30185  wkslem1  30188  uspgr2wlkeq  30226  wlkdlem2  30262  upgrwlkdvdelem  30322  crctcshwlkn0lem2  30400  crctcshwlkn0lem3  30401  crctcshwlkn0lem4  30402  crctcshwlkn0lem5  30403  wlkiswwlks2lem2  30459  wlkiswwlks2lem5  30462  wwlksnext  30482  wwlksnredwwlkn  30484  wwlksnextproplem2  30499  clwwlkccatlem  30580  clwlkclwwlklem2a1  30583  clwlkclwwlklem2fv1  30586  clwlkclwwlklem2a4  30588  clwlkclwwlklem2a  30589  clwlkclwwlklem2  30591  clwwisshclwwslemlem  30604  clwwisshclwws  30606  clwwlknlbonbgr1  30630  clwwlkel  30637  clwwlkf  30638  clwwlkwwlksb  30645  clwwlkext2edg  30647  wwlksext2clwwlk  30648  clwwlknonex2lem2  30699  eupthseg  30807  upgreupthseg  30810  eupth2lem3  30837  2clwwlk2clwwlklem  30947  2clwwlk  30948  numclwwlk1lem2f1  30958  numclwlk1lem2  30971  nvs  31265  nvtri  31272  ipval  31305  blocnilem  31406  phpar2  31425  phpar  31426  sii  31456  normsub0  31738  norm-ii  31740  norm-iii  31742  normsub  31745  normpyth  31747  norm3dif  31752  norm3lemt  31754  norm3adifi  31755  normpar  31757  polid  31761  bcs  31783  pjaddi  32288  pjsubi  32290  pjmuli  32291  pjcjt2  32294  lnopeq0lem2  32608  lnopunilem2  32613  branmfn  32707  hstel2  32821  stj  32837  cdj3lem1  33036  cdj3lem2b  33039  cdj3lem3b  33042  cdj3i  33043  ccatws1f1o  33514  gsummulsubdishift1  33629  elrgspnlem2  33804  selvply1rhmlemb  34151  constrsuc  34370  cnre2csqlem  34542  cnre2csqima  34543  mndpluscn  34558  lmdvg  34585  signsvfn  35211  subfacval2  35952  cvmliftlem7  36056  elmrsubrn  36285  faclim2  36513  fwddifval  36927  fwddifnval  36928  dnival  37337  unblimceq0lem  37372  unbdqndv2  37377  poimirlem32  38570  itg2gt0cn  38593  ftc1cnnclem  38609  ftc1cnnc  38610  areacirc  38631  sdclem1  38677  fdc  38679  seqpo  38681  incsequz  38682  incsequz2  38683  mettrifi  38691  caushft  38695  bfplem1  38756  ghomco  38825  rngohomadd  38903  rngohommul  38904  dihval  42289  lclkrlem1  42563  hdmap14lem2a  42924  hgmapval  42944  deg1pow  43191  sticksstones10  43205  sticksstones12a  43207  abvexp  43596  fsuppind  43618  prjspnval  43644  incssnn0  43721  rencldnfilem  43826  irrapxlem5  43832  irrapxlem6  43833  pellexlem3  43837  cvgdvgrat  45296  radcnvrat  45297  hashnzfzclim  45305  binomcxplemradcnv  45335  iunincfi  46108  monoords  46312  fperiodmullem  46318  monoordxrv  46490  monoordxr  46491  monoord2xrv  46492  monoord2xr  46493  climinf  46617  climsuse  46619  climinff  46622  mullimc  46627  mullimcf  46634  idlimc  46637  limcperiod  46639  limcrecl  46640  limclner  46660  climinf2  46716  climxrrelem  46758  cnrefiisplem  46838  cnrefiisp  46839  climxlim2lem  46854  cncfshift  46883  cncfperiod  46888  fperdvper  46928  dvnmul  46952  iblspltprt  46982  itgspltprt  46988  itgiccshift  46989  itgperiod  46990  dirkerval2  47103  dirkertrigeqlem1  47107  dirkertrigeqlem2  47108  dirkertrigeqlem3  47109  dirkercncflem2  47113  dirkercncflem3  47114  fourierdlem29  47145  fourierdlem48  47163  fourierdlem49  47164  fourierdlem113  47228  elaa2lem  47242  elaa2  47243  nnfoctbdj  47465  meaiuninclem  47489  meaiunincf  47492  meaiuninc3v  47493  meaiuninc3  47494  meaiininclem  47495  meaiininc  47496  smflimlem6  47785  ormkglobd  47886  2ltceilhalf  48401  ceilhalfnn  48409  smonoord  48446  iccpartimp  48498  iccelpart  48514  icceuelpart  48517  fargshiftfv  48520  fmtnorec2  48627  ppivalnnnprmge6  48710  ppivalnnnprm  48712  ppivalnn  48716  bgoldbtbndlem2  48903  bgoldbtbndlem3  48904  bgoldbtbnd  48906  upgrimwlklem5  48998  gpgov  49139  gpg5nbgrvtx13starlem2  49169  ply1mulgsumlem3  49499  ply1mulgsumlem4  49500  ply1mulgsum  49501  ackvalsuc1  49790