Theorem fvoveq1 7426

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

Syntax hints:   → wi 4   = wceq 1540  ‘cfv 6530  (class class class)co 7403

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-ov 7406

This theorem is referenced by:  coof  7693  eluzaddOLD  12885  eluzsubOLD  12886  fldiv4p1lem1div2  13850  fldiv4lem1div2  13852  modval  13886  seqval  14028  seqp1  14032  seqshft2  14044  monoord  14048  monoord2  14049  seqhomo  14065  facp1  14294  faclbnd4lem2  14310  bcval  14320  lsw0  14581  ccatval1  14593  ccatval2  14594  ccatalpha  14609  swrdfv  14664  2swrd2eqwrdeq  14970  imval  15124  recan  15353  rlimcld2  15592  rlimcn1  15602  rlimcn3  15604  climcn1  15606  climcn2  15607  subcn2  15609  o1of2  15627  isercoll2  15683  climsup  15684  serf0  15695  iseraltlem2  15697  fsumrelem  15821  mertenslem1  15898  mertenslem2  15899  mertens  15900  bitsfval  16440  smuval  16498  pcfac  16917  vdwlem6  17004  vdwlem8  17006  vdwlem9  17007  vdwlem10  17008  imasaddvallem  17541  imasvscafn  17549  imasvscaval  17550  mgmhmlin  18675  mhmlin  18769  mhmlem  19043  mulginvcom  19080  mhmmulg  19096  ghmlin  19202  efgsdm  19709  efgsdmi  19711  efgsrel  19713  efgsp1  19716  frgpup1  19754  rnghmmul  20407  c0snmgmhm  20420  zrrnghm  20494  abvmul  20779  abvtri  20780  issrngd  20813  lmhmlin  20991  ipcj  21592  psrmulval  21902  mhpmulcl  22085  psdcoef  22096  psdadd  22099  psdpw  22106  coe1mul2  22204  coe1tmmul2fv  22213  coe1pwmulfv  22215  cply1mul  22232  mat1scmat  22475  mdetmul  22559  madufval  22573  cramer0  22626  cpmatmcllem  22654  d1mat2pmat  22675  m2cpminvid2lem  22690  decpmatmullem  22707  decpmatmulsumfsupp  22709  pm2mpmhmlem1  22754  pm2mpmhmlem2  22755  cayhamlem1  22802  cpmadumatpoly  22819  cayleyhamilton  22826  1stcelcls  23397  imasdsf1olem  24310  comet  24450  nrmmetd  24511  tngngp  24591  tngngp3  24593  nmvs  24613  mulc1cncf  24847  cncfco  24849  pi1xfr  25004  pi1coghm  25010  caubl  25258  caublcls  25259  bcthlem2  25275  bcthlem3  25276  bcthlem4  25277  bcthlem5  25278  ivthlem2  25403  ovolicc2lem4  25471  volsuplem  25506  volsup  25507  uniioombllem3  25536  itg1climres  25665  itg2monolem1  25701  itg2i1fseqle  25705  itg2i1fseq  25706  itg2i1fseq2  25707  itg2addlem  25709  itgeq2  25729  dvferm1lem  25938  dvferm2lem  25940  dvlip  25948  c1lip1  25952  lhop1lem  25968  lhop1  25969  ftc1lem4  25996  ftc1lem6  25998  mdegmullem  26033  coe1mul3  26054  ply1divex  26092  coeeu  26180  coeeq  26182  coemullem  26205  coemul  26207  dvply1  26241  dvply2g  26242  dvply2gOLD  26243  aalioulem3  26292  aaliou3lem8  26303  ulmshftlem  26348  ulmshft  26349  ulmss  26356  pserdvlem2  26388  cxpcn3lem  26707  loglesqrt  26721  birthdaylem2  26912  emcllem2  26957  emcllem3  26958  harmonicbnd2  26965  lgamgulmlem2  26990  lgamgulmlem3  26991  lgamgulmlem5  26993  lgambdd  26997  lgamcvglem  27000  facgam  27026  ftalem7  27039  bposlem7  27251  bposlem9  27253  lgsqrlem2  27308  lgsqrlem4  27310  2lgslem3a  27357  2lgslem3b  27358  2lgslem3c  27359  2lgslem3d  27360  rplogsumlem1  27445  dchrvmasumlem1  27456  logsqvma  27503  logsqvma2  27504  selberglem3  27508  selberg  27509  selberg2lem  27511  selberg4lem1  27521  pntrsumo1  27526  selberg34r  27532  pntsval  27533  pntsval2  27537  pntrlog2bndlem1  27538  pntrlog2bndlem4  27541  pntpbnd  27549  pntibnd  27554  pntlemo  27568  addsbday  27967  seqsval  28211  seqsp1  28234  zs12bday  28341  ewlkinedg  29530  wkslem1  29533  uspgr2wlkeq  29572  wlkdlem2  29609  upgrwlkdvdelem  29664  crctcshwlkn0lem2  29739  crctcshwlkn0lem3  29740  crctcshwlkn0lem4  29741  crctcshwlkn0lem5  29742  wlkiswwlks2lem2  29798  wlkiswwlks2lem5  29801  wwlksnext  29821  wwlksnredwwlkn  29823  wwlksnextproplem2  29838  clwwlkccatlem  29916  clwlkclwwlklem2a1  29919  clwlkclwwlklem2fv1  29922  clwlkclwwlklem2a4  29924  clwlkclwwlklem2a  29925  clwlkclwwlklem2  29927  clwwisshclwwslemlem  29940  clwwisshclwws  29942  clwwlknlbonbgr1  29966  clwwlkel  29973  clwwlkf  29974  clwwlkwwlksb  29981  clwwlkext2edg  29983  wwlksext2clwwlk  29984  clwwlknonex2lem2  30035  eupthseg  30133  upgreupthseg  30136  eupth2lem3  30163  2clwwlk2clwwlklem  30273  2clwwlk  30274  numclwwlk1lem2f1  30284  numclwlk1lem2  30297  nvs  30590  nvtri  30597  ipval  30630  blocnilem  30731  phpar2  30750  phpar  30751  sii  30781  normsub0  31063  norm-ii  31065  norm-iii  31067  normsub  31070  normpyth  31072  norm3dif  31077  norm3lemt  31079  norm3adifi  31080  normpar  31082  polid  31086  bcs  31108  pjaddi  31613  pjsubi  31615  pjmuli  31616  pjcjt2  31619  lnopeq0lem2  31933  lnopunilem2  31938  branmfn  32032  hstel2  32146  stj  32162  cdj3lem1  32361  cdj3lem2b  32364  cdj3lem3b  32367  cdj3i  32368  ccatws1f1o  32873  chnltm1  32934  chnind  32937  elrgspnlem2  33184  constrsuc  33718  cnre2csqlem  33887  cnre2csqima  33888  mndpluscn  33903  lmdvg  33930  plymulx  34526  signsvfn  34560  subfacval2  35155  cvmliftlem7  35259  elmrsubrn  35488  faclim2  35711  fwddifval  36126  fwddifnval  36127  dnival  36435  unblimceq0lem  36470  unbdqndv2  36475  matunitlindf  37588  poimirlem32  37622  itg2gt0cn  37645  ftc1cnnclem  37661  ftc1cnnc  37662  areacirc  37683  sdclem1  37713  fdc  37715  seqpo  37717  incsequz  37718  incsequz2  37719  mettrifi  37727  caushft  37731  bfplem1  37792  ghomco  37861  rngohomadd  37939  rngohommul  37940  dihval  41197  lclkrlem1  41471  hdmap14lem2a  41832  hgmapval  41852  deg1pow  42100  sticksstones10  42114  sticksstones12a  42116  abvexp  42502  fsuppind  42560  prjspnval  42586  incssnn0  42681  rencldnfilem  42790  irrapxlem5  42796  irrapxlem6  42797  pellexlem3  42801  cvgdvgrat  44285  radcnvrat  44286  hashnzfzclim  44294  binomcxplemradcnv  44324  iunincfi  45066  monoords  45274  fperiodmullem  45280  monoordxrv  45456  monoordxr  45457  monoord2xrv  45458  monoord2xr  45459  climinf  45583  climsuse  45585  climinff  45588  mullimc  45593  mullimcf  45600  idlimc  45603  limcperiod  45605  limcrecl  45606  limclner  45628  climinf2  45684  climxrrelem  45726  cnrefiisplem  45806  cnrefiisp  45807  climxlim2lem  45822  cncfshift  45851  cncfperiod  45856  fperdvper  45896  dvnmul  45920  iblspltprt  45950  itgspltprt  45956  itgiccshift  45957  itgperiod  45958  dirkerval2  46071  dirkertrigeqlem1  46075  dirkertrigeqlem2  46076  dirkertrigeqlem3  46077  dirkercncflem2  46081  dirkercncflem3  46082  fourierdlem29  46113  elaa2lem  46210  elaa2  46211  nnfoctbdj  46433  meaiuninclem  46457  meaiunincf  46460  meaiuninc3v  46461  meaiuninc3  46462  meaiininclem  46463  meaiininc  46464  smflimlem6  46753  ormkglobd  46852  natglobalincr  46854  tworepnotupword  46863  2ltceilhalf  47305  ceilhalfnn  47313  smonoord  47333  iccpartimp  47379  iccelpart  47395  icceuelpart  47398  fargshiftfv  47401  fmtnorec2  47505  bgoldbtbndlem2  47768  bgoldbtbndlem3  47769  bgoldbtbnd  47771  upgrimwlklem5  47862  gpgov  47994  gpg5nbgrvtx13starlem2  48022  ply1mulgsumlem3  48312  ply1mulgsumlem4  48313  ply1mulgsum  48314  ackvalsuc1  48607