Theorem fvoveq1 7453

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

Syntax hints:   → wi 4   = wceq 1536  ‘cfv 6562  (class class class)co 7430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433

This theorem is referenced by:  coof  7720  eluzaddOLD  12910  eluzsubOLD  12911  fldiv4p1lem1div2  13871  fldiv4lem1div2  13873  modval  13907  seqval  14049  seqp1  14053  seqshft2  14065  monoord  14069  monoord2  14070  seqhomo  14086  facp1  14313  faclbnd4lem2  14329  bcval  14339  lsw0  14599  ccatval1  14611  ccatval2  14612  ccatalpha  14627  swrdfv  14682  2swrd2eqwrdeq  14988  imval  15142  recan  15371  rlimcld2  15610  rlimcn1  15620  rlimcn3  15622  climcn1  15624  climcn2  15625  subcn2  15627  o1of2  15645  isercoll2  15701  climsup  15702  serf0  15713  iseraltlem2  15715  fsumrelem  15839  mertenslem1  15916  mertenslem2  15917  mertens  15918  bitsfval  16456  smuval  16514  pcfac  16932  vdwlem6  17019  vdwlem8  17021  vdwlem9  17022  vdwlem10  17023  imasaddvallem  17575  imasvscafn  17583  imasvscaval  17584  mgmhmlin  18724  mhmlin  18818  mhmlem  19092  mulginvcom  19129  mhmmulg  19145  ghmlin  19251  efgsdm  19762  efgsdmi  19764  efgsrel  19766  efgsp1  19769  frgpup1  19807  rnghmmul  20465  c0snmgmhm  20478  zrrnghm  20552  abvmul  20838  abvtri  20839  issrngd  20872  lmhmlin  21051  ipcj  21669  psrmulval  21981  mhpmulcl  22170  psdcoef  22181  psdadd  22184  coe1mul2  22287  coe1tmmul2fv  22296  coe1pwmulfv  22298  cply1mul  22315  mat1scmat  22560  mdetmul  22644  madufval  22658  cramer0  22711  cpmatmcllem  22739  d1mat2pmat  22760  m2cpminvid2lem  22775  decpmatmullem  22792  decpmatmulsumfsupp  22794  pm2mpmhmlem1  22839  pm2mpmhmlem2  22840  cayhamlem1  22887  cpmadumatpoly  22904  cayleyhamilton  22911  1stcelcls  23484  imasdsf1olem  24398  comet  24541  nrmmetd  24602  tngngp  24690  tngngp3  24692  nmvs  24712  mulc1cncf  24944  cncfco  24946  pi1xfr  25101  pi1coghm  25107  caubl  25355  caublcls  25356  bcthlem2  25372  bcthlem3  25373  bcthlem4  25374  bcthlem5  25375  ivthlem2  25500  ovolicc2lem4  25568  volsuplem  25603  volsup  25604  uniioombllem3  25633  itg1climres  25763  itg2monolem1  25799  itg2i1fseqle  25803  itg2i1fseq  25804  itg2i1fseq2  25805  itg2addlem  25807  itgeq2  25827  dvferm1lem  26036  dvferm2lem  26038  dvlip  26046  c1lip1  26050  lhop1lem  26066  lhop1  26067  ftc1lem4  26094  ftc1lem6  26096  mdegmullem  26131  coe1mul3  26152  ply1divex  26190  coeeu  26278  coeeq  26280  coemullem  26303  coemul  26305  dvply1  26339  dvply2g  26340  dvply2gOLD  26341  aalioulem3  26390  aaliou3lem8  26401  ulmshftlem  26446  ulmshft  26447  ulmss  26454  pserdvlem2  26486  cxpcn3lem  26804  loglesqrt  26818  birthdaylem2  27009  emcllem2  27054  emcllem3  27055  harmonicbnd2  27062  lgamgulmlem2  27087  lgamgulmlem3  27088  lgamgulmlem5  27090  lgambdd  27094  lgamcvglem  27097  facgam  27123  ftalem7  27136  bposlem7  27348  bposlem9  27350  lgsqrlem2  27405  lgsqrlem4  27407  2lgslem3a  27454  2lgslem3b  27455  2lgslem3c  27456  2lgslem3d  27457  rplogsumlem1  27542  dchrvmasumlem1  27553  logsqvma  27600  logsqvma2  27601  selberglem3  27605  selberg  27606  selberg2lem  27608  selberg4lem1  27618  pntrsumo1  27623  selberg34r  27629  pntsval  27630  pntsval2  27634  pntrlog2bndlem1  27635  pntrlog2bndlem4  27638  pntpbnd  27646  pntibnd  27651  pntlemo  27665  addsbday  28064  seqsval  28308  seqsp1  28331  zs12bday  28438  ewlkinedg  29636  wkslem1  29639  uspgr2wlkeq  29678  wlkdlem2  29715  upgrwlkdvdelem  29768  crctcshwlkn0lem2  29840  crctcshwlkn0lem3  29841  crctcshwlkn0lem4  29842  crctcshwlkn0lem5  29843  wlkiswwlks2lem2  29899  wlkiswwlks2lem5  29902  wwlksnext  29922  wwlksnredwwlkn  29924  wwlksnextproplem2  29939  clwwlkccatlem  30017  clwlkclwwlklem2a1  30020  clwlkclwwlklem2fv1  30023  clwlkclwwlklem2a4  30025  clwlkclwwlklem2a  30026  clwlkclwwlklem2  30028  clwwisshclwwslemlem  30041  clwwisshclwws  30043  clwwlknlbonbgr1  30067  clwwlkel  30074  clwwlkf  30075  clwwlkwwlksb  30082  clwwlkext2edg  30084  wwlksext2clwwlk  30085  clwwlknonex2lem2  30136  eupthseg  30234  upgreupthseg  30237  eupth2lem3  30264  2clwwlk2clwwlklem  30374  2clwwlk  30375  numclwwlk1lem2f1  30385  numclwlk1lem2  30398  nvs  30691  nvtri  30698  ipval  30731  blocnilem  30832  phpar2  30851  phpar  30852  sii  30882  normsub0  31164  norm-ii  31166  norm-iii  31168  normsub  31171  normpyth  31173  norm3dif  31178  norm3lemt  31180  norm3adifi  31181  normpar  31183  polid  31187  bcs  31209  pjaddi  31714  pjsubi  31716  pjmuli  31717  pjcjt2  31720  lnopeq0lem2  32034  lnopunilem2  32039  branmfn  32133  hstel2  32247  stj  32263  cdj3lem1  32462  cdj3lem2b  32465  cdj3lem3b  32468  cdj3i  32469  ccatws1f1o  32920  chnltm1  32982  chnind  32984  elrgspnlem2  33232  constrsuc  33742  cnre2csqlem  33870  cnre2csqima  33871  mndpluscn  33886  lmdvg  33913  plymulx  34541  signsvfn  34575  subfacval2  35171  cvmliftlem7  35275  elmrsubrn  35504  faclim2  35727  fwddifval  36143  fwddifnval  36144  dnival  36453  unblimceq0lem  36488  unbdqndv2  36493  matunitlindf  37604  poimirlem32  37638  itg2gt0cn  37661  ftc1cnnclem  37677  ftc1cnnc  37678  areacirc  37699  sdclem1  37729  fdc  37731  seqpo  37733  incsequz  37734  incsequz2  37735  mettrifi  37743  caushft  37747  bfplem1  37808  ghomco  37877  rngohomadd  37955  rngohommul  37956  dihval  41214  lclkrlem1  41488  hdmap14lem2a  41849  hgmapval  41869  deg1pow  42122  sticksstones10  42136  sticksstones12a  42138  abvexp  42518  fsuppind  42576  prjspnval  42602  incssnn0  42698  rencldnfilem  42807  irrapxlem5  42813  irrapxlem6  42814  pellexlem3  42818  cvgdvgrat  44308  radcnvrat  44309  hashnzfzclim  44317  binomcxplemradcnv  44347  iunincfi  45033  monoords  45247  fperiodmullem  45253  monoordxrv  45431  monoordxr  45432  monoord2xrv  45433  monoord2xr  45434  climinf  45561  climsuse  45563  climinff  45566  mullimc  45571  mullimcf  45578  idlimc  45581  limcperiod  45583  limcrecl  45584  limclner  45606  climinf2  45662  climxrrelem  45704  cnrefiisplem  45784  cnrefiisp  45785  climxlim2lem  45800  cncfshift  45829  cncfperiod  45834  fperdvper  45874  dvnmul  45898  iblspltprt  45928  itgspltprt  45934  itgiccshift  45935  itgperiod  45936  dirkerval2  46049  dirkertrigeqlem1  46053  dirkertrigeqlem2  46054  dirkertrigeqlem3  46055  dirkercncflem2  46059  dirkercncflem3  46060  fourierdlem29  46091  elaa2lem  46188  elaa2  46189  nnfoctbdj  46411  meaiuninclem  46435  meaiunincf  46438  meaiuninc3v  46439  meaiuninc3  46440  meaiininclem  46441  meaiininc  46442  smflimlem6  46731  natglobalincr  46830  tworepnotupword  46839  smonoord  47295  iccpartimp  47341  iccelpart  47357  icceuelpart  47360  fargshiftfv  47363  fmtnorec2  47467  bgoldbtbndlem2  47730  bgoldbtbndlem3  47731  bgoldbtbnd  47733  gpgov  47936  2ltceilhalf  47949  gpg5nbgrvtx13starlem2  47962  ply1mulgsumlem3  48233  ply1mulgsumlem4  48234  ply1mulgsum  48235  ackvalsuc1  48528