Theorem fvoveq1 7450

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

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

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 2838  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-br 5106  df-iota 6500  df-fv 6554  df-ov 7430

This theorem is used by:  coof  7724  fldiv4p1lem1div2  13985  fldiv4lem1div2  13987  modval  14021  seqval  14165  seqp1  14169  seqshft2  14181  monoord  14185  monoord2  14186  seqhomo  14202  facp1  14432  faclbnd4lem2  14448  bcval  14458  lsw0  14720  ccatval1  14732  ccatval2  14733  ccatalpha  14750  swrdfv  14807  2swrd2eqwrdeq  15118  imval  15286  recan  15516  rlimcld2  15757  rlimcn1  15767  rlimcn3  15769  climcn1  15771  climcn2  15772  subcn2  15774  o1of2  15792  isercoll2  15848  climsup  15849  serf0  15860  iseraltlem2  15862  fsumrelem  15986  mertenslem1  16065  mertenslem2  16066  mertens  16067  bitsfval  16605  smuval  16663  pcfac  17089  vdwlem6  17176  vdwlem8  17178  vdwlem9  17179  vdwlem10  17180  imasaddvallem  17713  imasvscafn  17721  imasvscaval  17722  chnltm1  18795  chnind  18807  mgmhmlin  18900  mhmlin  19000  mhmlem  19284  mulginvcom  19321  mhmmulg  19337  ghmlin  19447  efgsdm  19956  efgsdmi  19958  efgsrel  19960  efgsp1  19963  frgpup1  20001  rnghmmul  20691  c0snmgmhm  20704  zrrnghm  20800  abvmul  21090  abvtri  21091  issrngd  21124  lmhmlin  21322  ipcj  21952  psrmulval  22264  mhpmulcl  22482  psdcoef  22493  psdadd  22496  psdpw  22503  coe1mul2  22600  coe1tmmul2fv  22609  coe1pwmulfv  22611  cply1mul  22626  mat1scmat  22866  mdetmul  22950  madufval  22964  matunitlindf  23008  cramer0  23020  cpmatmcllem  23048  d1mat2pmat  23069  m2cpminvid2lem  23084  decpmatmullem  23101  decpmatmulsumfsupp  23103  pm2mpmhmlem1  23148  pm2mpmhmlem2  23149  cayhamlem1  23196  cpmadumatpoly  23213  cayleyhamilton  23220  1stcelcls  23792  imasdsf1olem  24704  comet  24844  nrmmetd  24905  tngngp  24985  tngngp3  24987  nmvs  25007  mulc1cncf  25238  cncfco  25240  pi1xfr  25388  pi1coghm  25394  caubl  25641  caublcls  25642  bcthlem2  25658  bcthlem3  25659  bcthlem4  25660  bcthlem5  25661  ivthlem2  25785  ovolicc2lem4  25853  volsuplem  25888  volsup  25889  uniioombllem3  25918  itg1climres  26047  itg2monolem1  26083  itg2i1fseqle  26087  itg2i1fseq  26088  itg2i1fseq2  26089  itg2addlem  26091  itgeq2  26110  dvferm1lem  26316  dvferm2lem  26318  dvlip  26325  c1lip1  26329  lhop1lem  26345  lhop1  26346  ftc1lem4  26371  ftc1lem6  26373  mdegmullem  26408  coe1mul3  26429  ply1divex  26467  coeeu  26556  coeeq  26558  coemullem  26581  coemul  26583  plymulidp  26615  dvply1  26617  dvply2g  26618  aalioulem3  26673  aaliou3lem8  26684  ulmshftlem  26728  ulmshft  26729  ulmss  26736  pserdvlem2  26767  cxpcn3lem  27087  loglesqrt  27101  birthdaylem2  27292  emcllem2  27336  emcllem3  27337  harmonicbnd2  27344  lgamgulmlem2  27369  lgamgulmlem3  27370  lgamgulmlem5  27372  lgambdd  27376  lgamcvglem  27379  facgam  27405  ftalem7  27418  bposlem7  27629  bposlem9  27631  lgsqrlem2  27686  lgsqrlem4  27688  2lgslem3a  27735  2lgslem3b  27736  2lgslem3c  27737  2lgslem3d  27738  rplogsumlem1  27823  dchrvmasumlem1  27834  logsqvma  27881  logsqvma2  27882  selberglem3  27886  selberg  27887  selberg2lem  27889  selberg4lem1  27899  pntrsumo1  27904  selberg34r  27910  pntsval  27911  pntsval2  27915  pntrlog2bndlem1  27916  pntrlog2bndlem4  27919  pntpbnd  27927  pntibnd  27932  pntlemo  27946  addbday  28416  addonbday  28677  seqsval  28686  seqsp1  28709  bdaypw2n0bndlem  28861  ewlkinedg  30197  wkslem1  30200  uspgr2wlkeq  30238  wlkdlem2  30274  upgrwlkdvdelem  30334  crctcshwlkn0lem2  30412  crctcshwlkn0lem3  30413  crctcshwlkn0lem4  30414  crctcshwlkn0lem5  30415  wlkiswwlks2lem2  30471  wlkiswwlks2lem5  30474  wwlksnext  30494  wwlksnredwwlkn  30496  wwlksnextproplem2  30511  clwwlkccatlem  30592  clwlkclwwlklem2a1  30595  clwlkclwwlklem2fv1  30598  clwlkclwwlklem2a4  30600  clwlkclwwlklem2a  30601  clwlkclwwlklem2  30603  clwwisshclwwslemlem  30616  clwwisshclwws  30618  clwwlknlbonbgr1  30642  clwwlkel  30649  clwwlkf  30650  clwwlkwwlksb  30657  clwwlkext2edg  30659  wwlksext2clwwlk  30660  clwwlknonex2lem2  30711  eupthseg  30819  upgreupthseg  30822  eupth2lem3  30849  2clwwlk2clwwlklem  30959  2clwwlk  30960  numclwwlk1lem2f1  30970  numclwlk1lem2  30983  nvs  31277  nvtri  31284  ipval  31317  blocnilem  31418  phpar2  31437  phpar  31438  sii  31468  normsub0  31750  norm-ii  31752  norm-iii  31754  normsub  31757  normpyth  31759  norm3dif  31764  norm3lemt  31766  norm3adifi  31767  normpar  31769  polid  31773  bcs  31795  pjaddi  32300  pjsubi  32302  pjmuli  32303  pjcjt2  32306  lnopeq0lem2  32620  lnopunilem2  32625  branmfn  32719  hstel2  32833  stj  32849  cdj3lem1  33048  cdj3lem2b  33051  cdj3lem3b  33054  cdj3i  33055  ccatws1f1o  33567  gsummulsubdishift1  33682  elrgspnlem2  33857  selvply1rhmlemb  34204  constrsuc  34423  cnre2csqlem  34595  cnre2csqima  34596  mndpluscn  34611  lmdvg  34638  signsvfn  35264  subfacval2  36073  cvmliftlem7  36177  elmrsubrn  36406  faclim2  36640  fwddifval  37054  fwddifnval  37055  dnival  37464  unblimceq0lem  37499  unbdqndv2  37504  poimirlem32  38710  itg2gt0cn  38733  ftc1cnnclem  38749  ftc1cnnc  38750  areacirc  38771  sdclem1  38817  fdc  38819  seqpo  38821  incsequz  38822  incsequz2  38823  mettrifi  38831  caushft  38835  bfplem1  38896  ghomco  38965  rngohomadd  39043  rngohommul  39044  dihval  42429  lclkrlem1  42703  hdmap14lem2a  43064  hgmapval  43084  deg1pow  43331  sticksstones10  43345  sticksstones12a  43347  abvexp  43736  fsuppind  43758  prjspnval  43784  incssnn0  43862  rencldnfilem  43967  irrapxlem5  43973  irrapxlem6  43974  pellexlem3  43978  cvgdvgrat  45437  radcnvrat  45438  hashnzfzclim  45446  binomcxplemradcnv  45476  iunincfi  46248  monoords  46452  fperiodmullem  46458  monoordxrv  46630  monoordxr  46631  monoord2xrv  46632  monoord2xr  46633  climinf  46757  climsuse  46759  climinff  46762  mullimc  46767  mullimcf  46774  idlimc  46777  limcperiod  46779  limcrecl  46780  limclner  46800  climinf2  46856  climxrrelem  46898  cnrefiisplem  46978  cnrefiisp  46979  climxlim2lem  46994  cncfshift  47023  cncfperiod  47028  fperdvper  47068  dvnmul  47092  iblspltprt  47122  itgspltprt  47128  itgiccshift  47129  itgperiod  47130  dirkerval2  47243  dirkertrigeqlem1  47247  dirkertrigeqlem2  47248  dirkertrigeqlem3  47249  dirkercncflem2  47253  dirkercncflem3  47254  fourierdlem29  47285  fourierdlem48  47303  fourierdlem49  47304  fourierdlem113  47368  elaa2lem  47382  elaa2  47383  nnfoctbdj  47605  meaiuninclem  47629  meaiunincf  47632  meaiuninc3v  47633  meaiuninc3  47634  meaiininclem  47635  meaiininc  47636  smflimlem6  47925  ormkglobd  48026  2ltceilhalf  48541  ceilhalfnn  48549  smonoord  48586  iccpartimp  48638  iccelpart  48654  icceuelpart  48657  fargshiftfv  48660  fmtnorec2  48767  ppivalnnnprmge6  48850  ppivalnnnprm  48852  ppivalnn  48856  bgoldbtbndlem2  49043  bgoldbtbndlem3  49044  bgoldbtbnd  49046  upgrimwlklem5  49138  gpgov  49279  gpg5nbgrvtx13starlem2  49309  ply1mulgsumlem3  49639  ply1mulgsumlem4  49640  ply1mulgsum  49641  ackvalsuc1  49930