Theorem fvoveq1 7330

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

Syntax hints:   → wi 4   = wceq 1539  ‘cfv 6458  (class class class)co 7307

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3287  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-br 5082  df-iota 6410  df-fv 6466  df-ov 7310

This theorem is referenced by:  eluzadd  12659  eluzsub  12660  fldiv4p1lem1div2  13601  fldiv4lem1div2  13603  modval  13637  seqval  13778  seqp1  13782  seqshft2  13795  monoord  13799  monoord2  13800  seqhomo  13816  facp1  14038  faclbnd4lem2  14054  bcval  14064  lsw0  14313  ccatval1  14326  ccatval1OLD  14327  ccatval2  14328  ccatalpha  14343  swrdfv  14406  2swrd2eqwrdeq  14711  imval  14863  recan  15093  rlimcld2  15332  rlimcn1  15342  rlimcn3  15344  climcn1  15346  climcn2  15347  subcn2  15349  o1of2  15367  isercoll2  15425  climsup  15426  serf0  15437  iseraltlem2  15439  fsumrelem  15564  mertenslem1  15641  mertenslem2  15642  mertens  15643  bitsfval  16175  smuval  16233  pcfac  16645  vdwlem6  16732  vdwlem8  16734  vdwlem9  16735  vdwlem10  16736  imasaddvallem  17285  imasvscafn  17293  imasvscaval  17294  mhmlin  18482  mhmlem  18740  mulginvcom  18773  mhmmulg  18789  ghmlin  18884  efgsdm  19381  efgsdmi  19383  efgsrel  19385  efgsp1  19388  frgpup1  19426  abvmul  20134  abvtri  20135  issrngd  20166  lmhmlin  20342  ipcj  20884  psrmulval  21200  mhpmulcl  21384  coe1mul2  21485  coe1tmmul2fv  21494  coe1pwmulfv  21496  cply1mul  21510  mat1scmat  21733  mdetmul  21817  madufval  21831  cramer0  21884  cpmatmcllem  21912  d1mat2pmat  21933  m2cpminvid2lem  21948  decpmatmullem  21965  decpmatmulsumfsupp  21967  pm2mpmhmlem1  22012  pm2mpmhmlem2  22013  cayhamlem1  22060  cpmadumatpoly  22077  cayleyhamilton  22084  1stcelcls  22657  imasdsf1olem  23571  comet  23714  nrmmetd  23775  tngngp  23863  tngngp3  23865  nmvs  23885  mulc1cncf  24113  cncfco  24115  pi1xfr  24263  pi1coghm  24269  caubl  24517  caublcls  24518  bcthlem2  24534  bcthlem3  24535  bcthlem4  24536  bcthlem5  24537  ivthlem2  24661  ovolicc2lem4  24729  volsuplem  24764  volsup  24765  uniioombllem3  24794  itg1climres  24924  itg2monolem1  24960  itg2i1fseqle  24964  itg2i1fseq  24965  itg2i1fseq2  24966  itg2addlem  24968  itgeq2  24987  dvferm1lem  25193  dvferm2lem  25195  dvlip  25202  c1lip1  25206  lhop1lem  25222  lhop1  25223  ftc1lem4  25248  ftc1lem6  25250  mdegmullem  25288  coe1mul3  25309  ply1divex  25346  coeeu  25431  coeeq  25433  coemullem  25456  coemul  25458  dvply1  25489  dvply2g  25490  aalioulem3  25539  aaliou3lem8  25550  ulmshftlem  25593  ulmshft  25594  ulmss  25601  pserdvlem2  25632  cxpcn3lem  25945  loglesqrt  25956  birthdaylem2  26147  emcllem2  26191  emcllem3  26192  harmonicbnd2  26199  lgamgulmlem2  26224  lgamgulmlem3  26225  lgamgulmlem5  26227  lgambdd  26231  lgamcvglem  26234  facgam  26260  ftalem7  26273  bposlem7  26483  bposlem9  26485  lgsqrlem2  26540  lgsqrlem4  26542  2lgslem3a  26589  2lgslem3b  26590  2lgslem3c  26591  2lgslem3d  26592  rplogsumlem1  26677  dchrvmasumlem1  26688  logsqvma  26735  logsqvma2  26736  selberglem3  26740  selberg  26741  selberg2lem  26743  selberg4lem1  26753  pntrsumo1  26758  selberg34r  26764  pntsval  26765  pntsval2  26769  pntrlog2bndlem1  26770  pntrlog2bndlem4  26773  pntpbnd  26781  pntibnd  26786  pntlemo  26800  ewlkinedg  28016  wkslem1  28019  uspgr2wlkeq  28058  wlkdlem2  28096  upgrwlkdvdelem  28149  crctcshwlkn0lem2  28221  crctcshwlkn0lem3  28222  crctcshwlkn0lem4  28223  crctcshwlkn0lem5  28224  wlkiswwlks2lem2  28280  wlkiswwlks2lem5  28283  wwlksnext  28303  wwlksnredwwlkn  28305  wwlksnextproplem2  28320  clwwlkccatlem  28398  clwlkclwwlklem2a1  28401  clwlkclwwlklem2fv1  28404  clwlkclwwlklem2a4  28406  clwlkclwwlklem2a  28407  clwlkclwwlklem2  28409  clwwisshclwwslemlem  28422  clwwisshclwws  28424  clwwlknlbonbgr1  28448  clwwlkel  28455  clwwlkf  28456  clwwlkwwlksb  28463  clwwlkext2edg  28465  wwlksext2clwwlk  28466  clwwlknonex2lem2  28517  eupthseg  28615  upgreupthseg  28618  eupth2lem3  28645  2clwwlk2clwwlklem  28755  2clwwlk  28756  numclwwlk1lem2f1  28766  numclwlk1lem2  28779  nvs  29070  nvtri  29077  ipval  29110  blocnilem  29211  phpar2  29230  phpar  29231  sii  29261  normsub0  29543  norm-ii  29545  norm-iii  29547  normsub  29550  normpyth  29552  norm3dif  29557  norm3lemt  29559  norm3adifi  29560  normpar  29562  polid  29566  bcs  29588  pjaddi  30093  pjsubi  30095  pjmuli  30096  pjcjt2  30099  lnopeq0lem2  30413  lnopunilem2  30418  branmfn  30512  hstel2  30626  stj  30642  cdj3lem1  30841  cdj3lem2b  30844  cdj3lem3b  30847  cdj3i  30848  cnre2csqlem  31905  cnre2csqima  31906  mndpluscn  31921  lmdvg  31948  plymulx  32572  signsvfn  32606  subfacval2  33194  cvmliftlem7  33298  elmrsubrn  33527  faclim2  33759  fwddifval  34509  fwddifnval  34510  dnival  34696  unblimceq0lem  34731  unbdqndv2  34736  matunitlindf  35819  poimirlem32  35853  itg2gt0cn  35876  ftc1cnnclem  35892  ftc1cnnc  35893  areacirc  35914  sdclem1  35945  fdc  35947  seqpo  35949  incsequz  35950  incsequz2  35951  mettrifi  35959  caushft  35963  bfplem1  36024  ghomco  36093  rngohomadd  36171  rngohommul  36172  dihval  39288  lclkrlem1  39562  hdmap14lem2a  39923  hgmapval  39943  sticksstones10  40153  sticksstones12a  40155  fsuppind  40316  prjspnval  40492  incssnn0  40570  rencldnfilem  40679  irrapxlem5  40685  irrapxlem6  40686  pellexlem3  40690  cvgdvgrat  41969  radcnvrat  41970  hashnzfzclim  41978  binomcxplemradcnv  42008  iunincfi  42682  monoords  42884  fperiodmullem  42890  monoordxrv  43070  monoordxr  43071  monoord2xrv  43072  monoord2xr  43073  climinf  43196  climsuse  43198  climinff  43201  mullimc  43206  mullimcf  43213  idlimc  43216  limcperiod  43218  limcrecl  43219  limclner  43241  climinf2  43297  climxrrelem  43339  cnrefiisplem  43419  cnrefiisp  43420  climxlim2lem  43435  cncfshift  43464  cncfperiod  43469  fperdvper  43509  dvnmul  43533  iblspltprt  43563  itgspltprt  43569  itgiccshift  43570  itgperiod  43571  dirkerval2  43684  dirkertrigeqlem1  43688  dirkertrigeqlem2  43689  dirkertrigeqlem3  43690  dirkercncflem2  43694  dirkercncflem3  43695  fourierdlem29  43726  elaa2lem  43823  elaa2  43824  nnfoctbdj  44044  meaiuninclem  44068  meaiunincf  44071  meaiuninc3v  44072  meaiuninc3  44073  meaiininclem  44074  meaiininc  44075  smflimlem6  44364  smonoord  44881  iccpartimp  44927  iccelpart  44943  icceuelpart  44946  fargshiftfv  44949  fmtnorec2  45053  bgoldbtbndlem2  45316  bgoldbtbndlem3  45317  bgoldbtbnd  45319  mgmhmlin  45398  rnghmmul  45516  c0snmgmhm  45530  zrrnghm  45533  ply1mulgsumlem3  45787  ply1mulgsumlem4  45788  ply1mulgsum  45789  ackvalsuc1  46083  natglobalincr  46570  tworepnotupword  46579