Theorem fvoveq1 7379

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

Syntax hints:   → wi 4   = wceq 1547  ‘cfv 6485  (class class class)co 7356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-iota 6441  df-fv 6493  df-ov 7359

This theorem is referenced by:  coof  7644  fldiv4p1lem1div2  13785  fldiv4lem1div2  13787  modval  13821  seqval  13965  seqp1  13969  seqshft2  13981  monoord  13985  monoord2  13986  seqhomo  14002  facp1  14231  faclbnd4lem2  14247  bcval  14257  lsw0  14518  ccatval1  14530  ccatval2  14531  ccatalpha  14547  swrdfv  14602  2swrd2eqwrdeq  14906  imval  15060  recan  15290  rlimcld2  15531  rlimcn1  15541  rlimcn3  15543  climcn1  15545  climcn2  15546  subcn2  15548  o1of2  15566  isercoll2  15622  climsup  15623  serf0  15634  iseraltlem2  15636  fsumrelem  15761  mertenslem1  15840  mertenslem2  15841  mertens  15842  bitsfval  16383  smuval  16441  pcfac  16861  vdwlem6  16948  vdwlem8  16950  vdwlem9  16951  vdwlem10  16952  imasaddvallem  17484  imasvscafn  17492  imasvscaval  17493  chnltm1  18566  chnind  18578  mgmhmlin  18658  mhmlin  18752  mhmlem  19029  mulginvcom  19066  mhmmulg  19082  ghmlin  19187  efgsdm  19696  efgsdmi  19698  efgsrel  19700  efgsp1  19703  frgpup1  19741  rnghmmul  20420  c0snmgmhm  20433  zrrnghm  20508  abvmul  20793  abvtri  20794  issrngd  20827  lmhmlin  21025  ipcj  21609  psrmulval  21919  mhpmulcl  22137  psdcoef  22148  psdadd  22151  psdpw  22158  coe1mul2  22255  coe1tmmul2fv  22264  coe1pwmulfv  22266  cply1mul  22282  mat1scmat  22522  mdetmul  22606  madufval  22620  cramer0  22673  cpmatmcllem  22701  d1mat2pmat  22722  m2cpminvid2lem  22737  decpmatmullem  22754  decpmatmulsumfsupp  22756  pm2mpmhmlem1  22801  pm2mpmhmlem2  22802  cayhamlem1  22849  cpmadumatpoly  22866  cayleyhamilton  22873  1stcelcls  23444  imasdsf1olem  24356  comet  24496  nrmmetd  24557  tngngp  24637  tngngp3  24639  nmvs  24659  mulc1cncf  24890  cncfco  24892  pi1xfr  25040  pi1coghm  25046  caubl  25293  caublcls  25294  bcthlem2  25310  bcthlem3  25311  bcthlem4  25312  bcthlem5  25313  ivthlem2  25437  ovolicc2lem4  25505  volsuplem  25540  volsup  25541  uniioombllem3  25570  itg1climres  25699  itg2monolem1  25735  itg2i1fseqle  25739  itg2i1fseq  25740  itg2i1fseq2  25741  itg2addlem  25743  itgeq2  25763  dvferm1lem  25969  dvferm2lem  25971  dvlip  25978  c1lip1  25982  lhop1lem  25998  lhop1  25999  ftc1lem4  26024  ftc1lem6  26026  mdegmullem  26061  coe1mul3  26082  ply1divex  26120  coeeu  26208  coeeq  26210  coemullem  26233  coemul  26235  dvply1  26268  dvply2g  26269  aalioulem3  26318  aaliou3lem8  26329  ulmshftlem  26372  ulmshft  26373  ulmss  26380  pserdvlem2  26411  cxpcn3lem  26729  loglesqrt  26743  birthdaylem2  26934  emcllem2  26978  emcllem3  26979  harmonicbnd2  26986  lgamgulmlem2  27011  lgamgulmlem3  27012  lgamgulmlem5  27014  lgambdd  27018  lgamcvglem  27021  facgam  27047  ftalem7  27060  bposlem7  27271  bposlem9  27273  lgsqrlem2  27328  lgsqrlem4  27330  2lgslem3a  27377  2lgslem3b  27378  2lgslem3c  27379  2lgslem3d  27380  rplogsumlem1  27465  dchrvmasumlem1  27476  logsqvma  27523  logsqvma2  27524  selberglem3  27528  selberg  27529  selberg2lem  27531  selberg4lem1  27541  pntrsumo1  27546  selberg34r  27552  pntsval  27553  pntsval2  27557  pntrlog2bndlem1  27558  pntrlog2bndlem4  27561  pntpbnd  27569  pntibnd  27574  pntlemo  27588  addbday  28028  addonbday  28289  seqsval  28298  seqsp1  28321  bdaypw2n0bndlem  28473  ewlkinedg  29691  wkslem1  29694  uspgr2wlkeq  29732  wlkdlem2  29768  upgrwlkdvdelem  29822  crctcshwlkn0lem2  29897  crctcshwlkn0lem3  29898  crctcshwlkn0lem4  29899  crctcshwlkn0lem5  29900  wlkiswwlks2lem2  29956  wlkiswwlks2lem5  29959  wwlksnext  29979  wwlksnredwwlkn  29981  wwlksnextproplem2  29996  clwwlkccatlem  30077  clwlkclwwlklem2a1  30080  clwlkclwwlklem2fv1  30083  clwlkclwwlklem2a4  30085  clwlkclwwlklem2a  30086  clwlkclwwlklem2  30088  clwwisshclwwslemlem  30101  clwwisshclwws  30103  clwwlknlbonbgr1  30127  clwwlkel  30134  clwwlkf  30135  clwwlkwwlksb  30142  clwwlkext2edg  30144  wwlksext2clwwlk  30145  clwwlknonex2lem2  30196  eupthseg  30294  upgreupthseg  30297  eupth2lem3  30324  2clwwlk2clwwlklem  30434  2clwwlk  30435  numclwwlk1lem2f1  30445  numclwlk1lem2  30458  nvs  30752  nvtri  30759  ipval  30792  blocnilem  30893  phpar2  30912  phpar  30913  sii  30943  normsub0  31225  norm-ii  31227  norm-iii  31229  normsub  31232  normpyth  31234  norm3dif  31239  norm3lemt  31241  norm3adifi  31242  normpar  31244  polid  31248  bcs  31270  pjaddi  31775  pjsubi  31777  pjmuli  31778  pjcjt2  31781  lnopeq0lem2  32095  lnopunilem2  32100  branmfn  32194  hstel2  32308  stj  32324  cdj3lem1  32523  cdj3lem2b  32526  cdj3lem3b  32529  cdj3i  32530  ccatws1f1o  33030  gsummulsubdishift1  33149  elrgspnlem2  33324  selvply1rhmlemb  33703  constrsuc  33922  cnre2csqlem  34094  cnre2csqima  34095  mndpluscn  34110  lmdvg  34137  plymulx  34732  signsvfn  34766  subfacval2  35415  cvmliftlem7  35519  elmrsubrn  35748  faclim2  35976  fwddifval  36390  fwddifnval  36391  dnival  36777  unblimceq0lem  36812  unbdqndv2  36817  matunitlindf  37985  poimirlem32  38019  itg2gt0cn  38042  ftc1cnnclem  38058  ftc1cnnc  38059  areacirc  38080  sdclem1  38110  fdc  38112  seqpo  38114  incsequz  38115  incsequz2  38116  mettrifi  38124  caushft  38128  bfplem1  38189  ghomco  38258  rngohomadd  38336  rngohommul  38337  dihval  41724  lclkrlem1  41998  hdmap14lem2a  42359  hgmapval  42379  deg1pow  42626  sticksstones10  42640  sticksstones12a  42642  abvexp  43018  fsuppind  43040  prjspnval  43066  incssnn0  43160  rencldnfilem  43265  irrapxlem5  43271  irrapxlem6  43272  pellexlem3  43276  cvgdvgrat  44757  radcnvrat  44758  hashnzfzclim  44766  binomcxplemradcnv  44796  iunincfi  45541  monoords  45745  fperiodmullem  45751  monoordxrv  45924  monoordxr  45925  monoord2xrv  45926  monoord2xr  45927  climinf  46051  climsuse  46053  climinff  46056  mullimc  46061  mullimcf  46068  idlimc  46071  limcperiod  46073  limcrecl  46074  limclner  46094  climinf2  46150  climxrrelem  46192  cnrefiisplem  46272  cnrefiisp  46273  climxlim2lem  46288  cncfshift  46317  cncfperiod  46322  fperdvper  46362  dvnmul  46386  iblspltprt  46416  itgspltprt  46422  itgiccshift  46423  itgperiod  46424  dirkerval2  46537  dirkertrigeqlem1  46541  dirkertrigeqlem2  46542  dirkertrigeqlem3  46543  dirkercncflem2  46547  dirkercncflem3  46548  fourierdlem29  46579  elaa2lem  46676  elaa2  46677  nnfoctbdj  46899  meaiuninclem  46923  meaiunincf  46926  meaiuninc3v  46927  meaiuninc3  46928  meaiininclem  46929  meaiininc  46930  smflimlem6  47219  ormkglobd  47320  natglobalincr  47322  2ltceilhalf  47795  ceilhalfnn  47803  smonoord  47840  iccpartimp  47892  iccelpart  47908  icceuelpart  47911  fargshiftfv  47914  fmtnorec2  48021  ppivalnnnprmge6  48104  ppivalnnnprm  48106  ppivalnn  48110  bgoldbtbndlem2  48297  bgoldbtbndlem3  48298  bgoldbtbnd  48300  upgrimwlklem5  48392  gpgov  48533  gpg5nbgrvtx13starlem2  48563  ply1mulgsumlem3  48879  ply1mulgsumlem4  48880  ply1mulgsum  48881  ackvalsuc1  49170