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 22	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	fvoveq1d 7433	1 ⊢ (𝐴 = 𝐵 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶)))

Syntax hints:   → wi 4   = wceq 1539  ‘cfv 6542  (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 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6494  df-fv 6550  df-ov 7414

This theorem is referenced by:  eluzaddOLD  12861  eluzsubOLD  12862  fldiv4p1lem1div2  13804  fldiv4lem1div2  13806  modval  13840  seqval  13981  seqp1  13985  seqshft2  13998  monoord  14002  monoord2  14003  seqhomo  14019  facp1  14242  faclbnd4lem2  14258  bcval  14268  lsw0  14519  ccatval1  14531  ccatval2  14532  ccatalpha  14547  swrdfv  14602  2swrd2eqwrdeq  14908  imval  15058  recan  15287  rlimcld2  15526  rlimcn1  15536  rlimcn3  15538  climcn1  15540  climcn2  15541  subcn2  15543  o1of2  15561  isercoll2  15619  climsup  15620  serf0  15631  iseraltlem2  15633  fsumrelem  15757  mertenslem1  15834  mertenslem2  15835  mertens  15836  bitsfval  16368  smuval  16426  pcfac  16836  vdwlem6  16923  vdwlem8  16925  vdwlem9  16926  vdwlem10  16927  imasaddvallem  17479  imasvscafn  17487  imasvscaval  17488  mgmhmlin  18624  mhmlin  18715  mhmlem  18981  mulginvcom  19015  mhmmulg  19031  ghmlin  19135  efgsdm  19639  efgsdmi  19641  efgsrel  19643  efgsp1  19646  frgpup1  19684  rnghmmul  20340  c0snmgmhm  20353  zrrnghm  20425  abvmul  20580  abvtri  20581  issrngd  20612  lmhmlin  20790  ipcj  21406  psrmulval  21724  mhpmulcl  21911  coe1mul2  22011  coe1tmmul2fv  22020  coe1pwmulfv  22022  cply1mul  22038  mat1scmat  22261  mdetmul  22345  madufval  22359  cramer0  22412  cpmatmcllem  22440  d1mat2pmat  22461  m2cpminvid2lem  22476  decpmatmullem  22493  decpmatmulsumfsupp  22495  pm2mpmhmlem1  22540  pm2mpmhmlem2  22541  cayhamlem1  22588  cpmadumatpoly  22605  cayleyhamilton  22612  1stcelcls  23185  imasdsf1olem  24099  comet  24242  nrmmetd  24303  tngngp  24391  tngngp3  24393  nmvs  24413  mulc1cncf  24645  cncfco  24647  pi1xfr  24802  pi1coghm  24808  caubl  25056  caublcls  25057  bcthlem2  25073  bcthlem3  25074  bcthlem4  25075  bcthlem5  25076  ivthlem2  25201  ovolicc2lem4  25269  volsuplem  25304  volsup  25305  uniioombllem3  25334  itg1climres  25464  itg2monolem1  25500  itg2i1fseqle  25504  itg2i1fseq  25505  itg2i1fseq2  25506  itg2addlem  25508  itgeq2  25527  dvferm1lem  25736  dvferm2lem  25738  dvlip  25745  c1lip1  25749  lhop1lem  25765  lhop1  25766  ftc1lem4  25791  ftc1lem6  25793  mdegmullem  25831  coe1mul3  25852  ply1divex  25889  coeeu  25974  coeeq  25976  coemullem  25999  coemul  26001  dvply1  26033  dvply2g  26034  aalioulem3  26083  aaliou3lem8  26094  ulmshftlem  26137  ulmshft  26138  ulmss  26145  pserdvlem2  26176  cxpcn3lem  26491  loglesqrt  26502  birthdaylem2  26693  emcllem2  26737  emcllem3  26738  harmonicbnd2  26745  lgamgulmlem2  26770  lgamgulmlem3  26771  lgamgulmlem5  26773  lgambdd  26777  lgamcvglem  26780  facgam  26806  ftalem7  26819  bposlem7  27029  bposlem9  27031  lgsqrlem2  27086  lgsqrlem4  27088  2lgslem3a  27135  2lgslem3b  27136  2lgslem3c  27137  2lgslem3d  27138  rplogsumlem1  27223  dchrvmasumlem1  27234  logsqvma  27281  logsqvma2  27282  selberglem3  27286  selberg  27287  selberg2lem  27289  selberg4lem1  27299  pntrsumo1  27304  selberg34r  27310  pntsval  27311  pntsval2  27315  pntrlog2bndlem1  27316  pntrlog2bndlem4  27319  pntpbnd  27327  pntibnd  27332  pntlemo  27346  ewlkinedg  29128  wkslem1  29131  uspgr2wlkeq  29170  wlkdlem2  29207  upgrwlkdvdelem  29260  crctcshwlkn0lem2  29332  crctcshwlkn0lem3  29333  crctcshwlkn0lem4  29334  crctcshwlkn0lem5  29335  wlkiswwlks2lem2  29391  wlkiswwlks2lem5  29394  wwlksnext  29414  wwlksnredwwlkn  29416  wwlksnextproplem2  29431  clwwlkccatlem  29509  clwlkclwwlklem2a1  29512  clwlkclwwlklem2fv1  29515  clwlkclwwlklem2a4  29517  clwlkclwwlklem2a  29518  clwlkclwwlklem2  29520  clwwisshclwwslemlem  29533  clwwisshclwws  29535  clwwlknlbonbgr1  29559  clwwlkel  29566  clwwlkf  29567  clwwlkwwlksb  29574  clwwlkext2edg  29576  wwlksext2clwwlk  29577  clwwlknonex2lem2  29628  eupthseg  29726  upgreupthseg  29729  eupth2lem3  29756  2clwwlk2clwwlklem  29866  2clwwlk  29867  numclwwlk1lem2f1  29877  numclwlk1lem2  29890  nvs  30183  nvtri  30190  ipval  30223  blocnilem  30324  phpar2  30343  phpar  30344  sii  30374  normsub0  30656  norm-ii  30658  norm-iii  30660  normsub  30663  normpyth  30665  norm3dif  30670  norm3lemt  30672  norm3adifi  30673  normpar  30675  polid  30679  bcs  30701  pjaddi  31206  pjsubi  31208  pjmuli  31209  pjcjt2  31212  lnopeq0lem2  31526  lnopunilem2  31531  branmfn  31625  hstel2  31739  stj  31755  cdj3lem1  31954  cdj3lem2b  31957  cdj3lem3b  31960  cdj3i  31961  cnre2csqlem  33188  cnre2csqima  33189  mndpluscn  33204  lmdvg  33231  plymulx  33857  signsvfn  33891  subfacval2  34476  cvmliftlem7  34580  elmrsubrn  34809  faclim2  35022  fwddifval  35438  fwddifnval  35439  dnival  35650  unblimceq0lem  35685  unbdqndv2  35690  matunitlindf  36789  poimirlem32  36823  itg2gt0cn  36846  ftc1cnnclem  36862  ftc1cnnc  36863  areacirc  36884  sdclem1  36914  fdc  36916  seqpo  36918  incsequz  36919  incsequz2  36920  mettrifi  36928  caushft  36932  bfplem1  36993  ghomco  37062  rngohomadd  37140  rngohommul  37141  dihval  40406  lclkrlem1  40680  hdmap14lem2a  41041  hgmapval  41061  sticksstones10  41277  sticksstones12a  41279  fsuppind  41464  prjspnval  41660  incssnn0  41751  rencldnfilem  41860  irrapxlem5  41866  irrapxlem6  41867  pellexlem3  41871  cvgdvgrat  43374  radcnvrat  43375  hashnzfzclim  43383  binomcxplemradcnv  43413  iunincfi  44084  monoords  44305  fperiodmullem  44311  monoordxrv  44490  monoordxr  44491  monoord2xrv  44492  monoord2xr  44493  climinf  44620  climsuse  44622  climinff  44625  mullimc  44630  mullimcf  44637  idlimc  44640  limcperiod  44642  limcrecl  44643  limclner  44665  climinf2  44721  climxrrelem  44763  cnrefiisplem  44843  cnrefiisp  44844  climxlim2lem  44859  cncfshift  44888  cncfperiod  44893  fperdvper  44933  dvnmul  44957  iblspltprt  44987  itgspltprt  44993  itgiccshift  44994  itgperiod  44995  dirkerval2  45108  dirkertrigeqlem1  45112  dirkertrigeqlem2  45113  dirkertrigeqlem3  45114  dirkercncflem2  45118  dirkercncflem3  45119  fourierdlem29  45150  elaa2lem  45247  elaa2  45248  nnfoctbdj  45470  meaiuninclem  45494  meaiunincf  45497  meaiuninc3v  45498  meaiuninc3  45499  meaiininclem  45500  meaiininc  45501  smflimlem6  45790  natglobalincr  45889  tworepnotupword  45898  smonoord  46337  iccpartimp  46383  iccelpart  46399  icceuelpart  46402  fargshiftfv  46405  fmtnorec2  46509  bgoldbtbndlem2  46772  bgoldbtbndlem3  46773  bgoldbtbnd  46775  ply1mulgsumlem3  47156  ply1mulgsumlem4  47157  ply1mulgsum  47158  ackvalsuc1  47452