Theorem fvoveq1 7419

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

Syntax hints:   → wi 4   = wceq 1560  ‘cfv 6521  (class class class)co 7396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6477  df-fv 6529  df-ov 7399

This theorem is referenced by:  coof  7684  fldiv4p1lem1div2  13845  fldiv4lem1div2  13847  modval  13881  seqval  14025  seqp1  14029  seqshft2  14041  monoord  14045  monoord2  14046  seqhomo  14062  facp1  14291  faclbnd4lem2  14307  bcval  14317  lsw0  14578  ccatval1  14590  ccatval2  14591  ccatalpha  14607  swrdfv  14662  2swrd2eqwrdeq  14966  imval  15134  recan  15364  rlimcld2  15605  rlimcn1  15615  rlimcn3  15617  climcn1  15619  climcn2  15620  subcn2  15622  o1of2  15640  isercoll2  15696  climsup  15697  serf0  15708  iseraltlem2  15710  fsumrelem  15835  mertenslem1  15914  mertenslem2  15915  mertens  15916  bitsfval  16457  smuval  16515  pcfac  16935  vdwlem6  17022  vdwlem8  17024  vdwlem9  17025  vdwlem10  17026  imasaddvallem  17559  imasvscafn  17567  imasvscaval  17568  chnltm1  18641  chnind  18653  mgmhmlin  18733  mhmlin  18827  mhmlem  19104  mulginvcom  19141  mhmmulg  19157  ghmlin  19261  efgsdm  19770  efgsdmi  19772  efgsrel  19774  efgsp1  19777  frgpup1  19815  rnghmmul  20498  c0snmgmhm  20511  zrrnghm  20586  abvmul  20870  abvtri  20871  issrngd  20904  lmhmlin  21102  ipcj  21686  psrmulval  21996  mhpmulcl  22214  psdcoef  22225  psdadd  22228  psdpw  22235  coe1mul2  22332  coe1tmmul2fv  22341  coe1pwmulfv  22343  cply1mul  22359  mat1scmat  22599  mdetmul  22683  madufval  22697  cramer0  22750  cpmatmcllem  22778  d1mat2pmat  22799  m2cpminvid2lem  22814  decpmatmullem  22831  decpmatmulsumfsupp  22833  pm2mpmhmlem1  22878  pm2mpmhmlem2  22879  cayhamlem1  22926  cpmadumatpoly  22943  cayleyhamilton  22950  1stcelcls  23521  imasdsf1olem  24433  comet  24573  nrmmetd  24634  tngngp  24714  tngngp3  24716  nmvs  24736  mulc1cncf  24967  cncfco  24969  pi1xfr  25117  pi1coghm  25123  caubl  25370  caublcls  25371  bcthlem2  25387  bcthlem3  25388  bcthlem4  25389  bcthlem5  25390  ivthlem2  25514  ovolicc2lem4  25582  volsuplem  25617  volsup  25618  uniioombllem3  25647  itg1climres  25776  itg2monolem1  25812  itg2i1fseqle  25816  itg2i1fseq  25817  itg2i1fseq2  25818  itg2addlem  25820  itgeq2  25840  dvferm1lem  26046  dvferm2lem  26048  dvlip  26055  c1lip1  26059  lhop1lem  26075  lhop1  26076  ftc1lem4  26101  ftc1lem6  26103  mdegmullem  26138  coe1mul3  26159  ply1divex  26197  coeeu  26285  coeeq  26287  coemullem  26310  coemul  26312  plymulidp  26346  dvply1  26348  dvply2g  26349  aalioulem3  26398  aaliou3lem8  26409  ulmshftlem  26452  ulmshft  26453  ulmss  26460  pserdvlem2  26491  cxpcn3lem  26812  loglesqrt  26826  birthdaylem2  27017  emcllem2  27061  emcllem3  27062  harmonicbnd2  27069  lgamgulmlem2  27094  lgamgulmlem3  27095  lgamgulmlem5  27097  lgambdd  27101  lgamcvglem  27104  facgam  27130  ftalem7  27143  bposlem7  27354  bposlem9  27356  lgsqrlem2  27411  lgsqrlem4  27413  2lgslem3a  27460  2lgslem3b  27461  2lgslem3c  27462  2lgslem3d  27463  rplogsumlem1  27548  dchrvmasumlem1  27559  logsqvma  27606  logsqvma2  27607  selberglem3  27611  selberg  27612  selberg2lem  27614  selberg4lem1  27624  pntrsumo1  27629  selberg34r  27635  pntsval  27636  pntsval2  27640  pntrlog2bndlem1  27641  pntrlog2bndlem4  27644  pntpbnd  27652  pntibnd  27657  pntlemo  27671  addbday  28111  addonbday  28372  seqsval  28381  seqsp1  28404  bdaypw2n0bndlem  28556  ewlkinedg  29805  wkslem1  29808  uspgr2wlkeq  29846  wlkdlem2  29882  upgrwlkdvdelem  29936  crctcshwlkn0lem2  30011  crctcshwlkn0lem3  30012  crctcshwlkn0lem4  30013  crctcshwlkn0lem5  30014  wlkiswwlks2lem2  30070  wlkiswwlks2lem5  30073  wwlksnext  30093  wwlksnredwwlkn  30095  wwlksnextproplem2  30110  clwwlkccatlem  30191  clwlkclwwlklem2a1  30194  clwlkclwwlklem2fv1  30197  clwlkclwwlklem2a4  30199  clwlkclwwlklem2a  30200  clwlkclwwlklem2  30202  clwwisshclwwslemlem  30215  clwwisshclwws  30217  clwwlknlbonbgr1  30241  clwwlkel  30248  clwwlkf  30249  clwwlkwwlksb  30256  clwwlkext2edg  30258  wwlksext2clwwlk  30259  clwwlknonex2lem2  30310  eupthseg  30408  upgreupthseg  30411  eupth2lem3  30438  2clwwlk2clwwlklem  30548  2clwwlk  30549  numclwwlk1lem2f1  30559  numclwlk1lem2  30572  nvs  30866  nvtri  30873  ipval  30906  blocnilem  31007  phpar2  31026  phpar  31027  sii  31057  normsub0  31339  norm-ii  31341  norm-iii  31343  normsub  31346  normpyth  31348  norm3dif  31353  norm3lemt  31355  norm3adifi  31356  normpar  31358  polid  31362  bcs  31384  pjaddi  31889  pjsubi  31891  pjmuli  31892  pjcjt2  31895  lnopeq0lem2  32209  lnopunilem2  32214  branmfn  32308  hstel2  32422  stj  32438  cdj3lem1  32637  cdj3lem2b  32640  cdj3lem3b  32643  cdj3i  32644  ccatws1f1o  33129  gsummulsubdishift1  33248  elrgspnlem2  33424  selvply1rhmlemb  33816  constrsuc  34035  cnre2csqlem  34207  cnre2csqima  34208  mndpluscn  34223  lmdvg  34250  signsvfn  34876  subfacval2  35537  cvmliftlem7  35641  elmrsubrn  35870  faclim2  36098  fwddifval  36512  fwddifnval  36513  dnival  36909  unblimceq0lem  36944  unbdqndv2  36949  matunitlindf  38117  poimirlem32  38151  itg2gt0cn  38174  ftc1cnnclem  38190  ftc1cnnc  38191  areacirc  38212  sdclem1  38242  fdc  38244  seqpo  38246  incsequz  38247  incsequz2  38248  mettrifi  38256  caushft  38260  bfplem1  38321  ghomco  38390  rngohomadd  38468  rngohommul  38469  dihval  41856  lclkrlem1  42130  hdmap14lem2a  42491  hgmapval  42511  deg1pow  42758  sticksstones10  42772  sticksstones12a  42774  abvexp  43150  fsuppind  43172  prjspnval  43198  incssnn0  43292  rencldnfilem  43397  irrapxlem5  43403  irrapxlem6  43404  pellexlem3  43408  cvgdvgrat  44889  radcnvrat  44890  hashnzfzclim  44898  binomcxplemradcnv  44928  iunincfi  45672  monoords  45876  fperiodmullem  45882  monoordxrv  46055  monoordxr  46056  monoord2xrv  46057  monoord2xr  46058  climinf  46182  climsuse  46184  climinff  46187  mullimc  46192  mullimcf  46199  idlimc  46202  limcperiod  46204  limcrecl  46205  limclner  46225  climinf2  46281  climxrrelem  46323  cnrefiisplem  46403  cnrefiisp  46404  climxlim2lem  46419  cncfshift  46448  cncfperiod  46453  fperdvper  46493  dvnmul  46517  iblspltprt  46547  itgspltprt  46553  itgiccshift  46554  itgperiod  46555  dirkerval2  46668  dirkertrigeqlem1  46672  dirkertrigeqlem2  46673  dirkertrigeqlem3  46674  dirkercncflem2  46678  dirkercncflem3  46679  fourierdlem29  46710  fourierdlem48  46728  fourierdlem49  46729  fourierdlem113  46793  elaa2lem  46807  elaa2  46808  nnfoctbdj  47030  meaiuninclem  47054  meaiunincf  47057  meaiuninc3v  47058  meaiuninc3  47059  meaiininclem  47060  meaiininc  47061  smflimlem6  47350  ormkglobd  47451  natglobalincr  47453  2ltceilhalf  47926  ceilhalfnn  47934  smonoord  47971  iccpartimp  48023  iccelpart  48039  icceuelpart  48042  fargshiftfv  48045  fmtnorec2  48152  ppivalnnnprmge6  48235  ppivalnnnprm  48237  ppivalnn  48241  bgoldbtbndlem2  48428  bgoldbtbndlem3  48429  bgoldbtbnd  48431  upgrimwlklem5  48523  gpgov  48664  gpg5nbgrvtx13starlem2  48694  ply1mulgsumlem3  49010  ply1mulgsumlem4  49011  ply1mulgsum  49012  ackvalsuc1  49301