Theorem fvoveq1 7434

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

Syntax hints:   → wi 4   = wceq 1567  ‘cfv 6537  (class class class)co 7411

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-ov 7414

This theorem is referenced by:  coof  7699  fldiv4p1lem1div2  13868  fldiv4lem1div2  13870  modval  13904  seqval  14048  seqp1  14052  seqshft2  14064  monoord  14068  monoord2  14069  seqhomo  14085  facp1  14314  faclbnd4lem2  14330  bcval  14340  lsw0  14602  ccatval1  14614  ccatval2  14615  ccatalpha  14631  swrdfv  14686  2swrd2eqwrdeq  14990  imval  15158  recan  15388  rlimcld2  15629  rlimcn1  15639  rlimcn3  15641  climcn1  15643  climcn2  15644  subcn2  15646  o1of2  15664  isercoll2  15720  climsup  15721  serf0  15732  iseraltlem2  15734  fsumrelem  15859  mertenslem1  15938  mertenslem2  15939  mertens  15940  bitsfval  16481  smuval  16539  pcfac  16959  vdwlem6  17046  vdwlem8  17048  vdwlem9  17049  vdwlem10  17050  imasaddvallem  17583  imasvscafn  17591  imasvscaval  17592  chnltm1  18665  chnind  18677  mgmhmlin  18757  mhmlin  18851  mhmlem  19128  mulginvcom  19165  mhmmulg  19181  ghmlin  19291  efgsdm  19800  efgsdmi  19802  efgsrel  19804  efgsp1  19807  frgpup1  19845  rnghmmul  20531  c0snmgmhm  20544  zrrnghm  20621  abvmul  20902  abvtri  20903  issrngd  20936  lmhmlin  21134  ipcj  21753  psrmulval  22063  mhpmulcl  22281  psdcoef  22292  psdadd  22295  psdpw  22302  coe1mul2  22399  coe1tmmul2fv  22408  coe1pwmulfv  22410  cply1mul  22425  mat1scmat  22665  mdetmul  22749  madufval  22763  cramer0  22816  cpmatmcllem  22844  d1mat2pmat  22865  m2cpminvid2lem  22880  decpmatmullem  22897  decpmatmulsumfsupp  22899  pm2mpmhmlem1  22944  pm2mpmhmlem2  22945  cayhamlem1  22992  cpmadumatpoly  23009  cayleyhamilton  23016  1stcelcls  23587  imasdsf1olem  24499  comet  24639  nrmmetd  24700  tngngp  24780  tngngp3  24782  nmvs  24802  mulc1cncf  25033  cncfco  25035  pi1xfr  25183  pi1coghm  25189  caubl  25436  caublcls  25437  bcthlem2  25453  bcthlem3  25454  bcthlem4  25455  bcthlem5  25456  ivthlem2  25580  ovolicc2lem4  25648  volsuplem  25683  volsup  25684  uniioombllem3  25713  itg1climres  25842  itg2monolem1  25878  itg2i1fseqle  25882  itg2i1fseq  25883  itg2i1fseq2  25884  itg2addlem  25886  itgeq2  25906  dvferm1lem  26112  dvferm2lem  26114  dvlip  26121  c1lip1  26125  lhop1lem  26141  lhop1  26142  ftc1lem4  26167  ftc1lem6  26169  mdegmullem  26204  coe1mul3  26225  ply1divex  26263  coeeu  26351  coeeq  26353  coemullem  26376  coemul  26378  plymulidp  26412  dvply1  26414  dvply2g  26415  aalioulem3  26464  aaliou3lem8  26475  ulmshftlem  26518  ulmshft  26519  ulmss  26526  pserdvlem2  26557  cxpcn3lem  26878  loglesqrt  26892  birthdaylem2  27083  emcllem2  27127  emcllem3  27128  harmonicbnd2  27135  lgamgulmlem2  27160  lgamgulmlem3  27161  lgamgulmlem5  27163  lgambdd  27167  lgamcvglem  27170  facgam  27196  ftalem7  27209  bposlem7  27420  bposlem9  27422  lgsqrlem2  27477  lgsqrlem4  27479  2lgslem3a  27526  2lgslem3b  27527  2lgslem3c  27528  2lgslem3d  27529  rplogsumlem1  27614  dchrvmasumlem1  27625  logsqvma  27672  logsqvma2  27673  selberglem3  27677  selberg  27678  selberg2lem  27680  selberg4lem1  27690  pntrsumo1  27695  selberg34r  27701  pntsval  27702  pntsval2  27706  pntrlog2bndlem1  27707  pntrlog2bndlem4  27710  pntpbnd  27718  pntibnd  27723  pntlemo  27737  addbday  28177  addonbday  28438  seqsval  28447  seqsp1  28470  bdaypw2n0bndlem  28622  ewlkinedg  29895  wkslem1  29898  uspgr2wlkeq  29936  wlkdlem2  29972  upgrwlkdvdelem  30026  crctcshwlkn0lem2  30101  crctcshwlkn0lem3  30102  crctcshwlkn0lem4  30103  crctcshwlkn0lem5  30104  wlkiswwlks2lem2  30160  wlkiswwlks2lem5  30163  wwlksnext  30183  wwlksnredwwlkn  30185  wwlksnextproplem2  30200  clwwlkccatlem  30281  clwlkclwwlklem2a1  30284  clwlkclwwlklem2fv1  30287  clwlkclwwlklem2a4  30289  clwlkclwwlklem2a  30290  clwlkclwwlklem2  30292  clwwisshclwwslemlem  30305  clwwisshclwws  30307  clwwlknlbonbgr1  30331  clwwlkel  30338  clwwlkf  30339  clwwlkwwlksb  30346  clwwlkext2edg  30348  wwlksext2clwwlk  30349  clwwlknonex2lem2  30400  eupthseg  30498  upgreupthseg  30501  eupth2lem3  30528  2clwwlk2clwwlklem  30638  2clwwlk  30639  numclwwlk1lem2f1  30649  numclwlk1lem2  30662  nvs  30956  nvtri  30963  ipval  30996  blocnilem  31097  phpar2  31116  phpar  31117  sii  31147  normsub0  31429  norm-ii  31431  norm-iii  31433  normsub  31436  normpyth  31438  norm3dif  31443  norm3lemt  31445  norm3adifi  31446  normpar  31448  polid  31452  bcs  31474  pjaddi  31979  pjsubi  31981  pjmuli  31982  pjcjt2  31985  lnopeq0lem2  32299  lnopunilem2  32304  branmfn  32398  hstel2  32512  stj  32528  cdj3lem1  32727  cdj3lem2b  32730  cdj3lem3b  32733  cdj3i  32734  ccatws1f1o  33212  gsummulsubdishift1  33329  elrgspnlem2  33504  selvply1rhmlemb  33854  constrsuc  34073  cnre2csqlem  34245  cnre2csqima  34246  mndpluscn  34261  lmdvg  34288  signsvfn  34914  subfacval2  35578  cvmliftlem7  35682  elmrsubrn  35911  faclim2  36139  fwddifval  36553  fwddifnval  36554  dnival  36949  unblimceq0lem  36984  unbdqndv2  36989  matunitlindf  38157  poimirlem32  38191  itg2gt0cn  38214  ftc1cnnclem  38230  ftc1cnnc  38231  areacirc  38252  sdclem1  38282  fdc  38284  seqpo  38286  incsequz  38287  incsequz2  38288  mettrifi  38296  caushft  38300  bfplem1  38361  ghomco  38430  rngohomadd  38508  rngohommul  38509  dihval  41896  lclkrlem1  42170  hdmap14lem2a  42531  hgmapval  42551  deg1pow  42798  sticksstones10  42812  sticksstones12a  42814  abvexp  43192  fsuppind  43214  prjspnval  43240  incssnn0  43334  rencldnfilem  43439  irrapxlem5  43445  irrapxlem6  43446  pellexlem3  43450  cvgdvgrat  44915  radcnvrat  44916  hashnzfzclim  44924  binomcxplemradcnv  44954  iunincfi  45704  monoords  45908  fperiodmullem  45914  monoordxrv  46087  monoordxr  46088  monoord2xrv  46089  monoord2xr  46090  climinf  46214  climsuse  46216  climinff  46219  mullimc  46224  mullimcf  46231  idlimc  46234  limcperiod  46236  limcrecl  46237  limclner  46257  climinf2  46313  climxrrelem  46355  cnrefiisplem  46435  cnrefiisp  46436  climxlim2lem  46451  cncfshift  46480  cncfperiod  46485  fperdvper  46525  dvnmul  46549  iblspltprt  46579  itgspltprt  46585  itgiccshift  46586  itgperiod  46587  dirkerval2  46700  dirkertrigeqlem1  46704  dirkertrigeqlem2  46705  dirkertrigeqlem3  46706  dirkercncflem2  46710  dirkercncflem3  46711  fourierdlem29  46742  fourierdlem48  46760  fourierdlem49  46761  fourierdlem113  46825  elaa2lem  46839  elaa2  46840  nnfoctbdj  47062  meaiuninclem  47086  meaiunincf  47089  meaiuninc3v  47090  meaiuninc3  47091  meaiininclem  47092  meaiininc  47093  smflimlem6  47382  ormkglobd  47483  natglobalincr  47485  2ltceilhalf  47958  ceilhalfnn  47966  smonoord  48003  iccpartimp  48055  iccelpart  48071  icceuelpart  48074  fargshiftfv  48077  fmtnorec2  48184  ppivalnnnprmge6  48267  ppivalnnnprm  48269  ppivalnn  48273  bgoldbtbndlem2  48460  bgoldbtbndlem3  48461  bgoldbtbnd  48463  upgrimwlklem5  48555  gpgov  48696  gpg5nbgrvtx13starlem2  48726  ply1mulgsumlem3  49053  ply1mulgsumlem4  49054  ply1mulgsum  49055  ackvalsuc1  49344