Theorem fvoveq1 7378

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

Syntax hints:   → wi 4   = wceq 1541  ‘cfv 6489  (class class class)co 7355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-iota 6445  df-fv 6497  df-ov 7358

This theorem is referenced by:  coof  7643  eluzaddOLD  12777  eluzsubOLD  12778  fldiv4p1lem1div2  13749  fldiv4lem1div2  13751  modval  13785  seqval  13929  seqp1  13933  seqshft2  13945  monoord  13949  monoord2  13950  seqhomo  13966  facp1  14195  faclbnd4lem2  14211  bcval  14221  lsw0  14482  ccatval1  14494  ccatval2  14495  ccatalpha  14511  swrdfv  14566  2swrd2eqwrdeq  14870  imval  15024  recan  15254  rlimcld2  15495  rlimcn1  15505  rlimcn3  15507  climcn1  15509  climcn2  15510  subcn2  15512  o1of2  15530  isercoll2  15586  climsup  15587  serf0  15598  iseraltlem2  15600  fsumrelem  15724  mertenslem1  15801  mertenslem2  15802  mertens  15803  bitsfval  16344  smuval  16402  pcfac  16821  vdwlem6  16908  vdwlem8  16910  vdwlem9  16911  vdwlem10  16912  imasaddvallem  17443  imasvscafn  17451  imasvscaval  17452  chnltm1  18525  chnind  18537  mgmhmlin  18617  mhmlin  18711  mhmlem  18985  mulginvcom  19022  mhmmulg  19038  ghmlin  19143  efgsdm  19652  efgsdmi  19654  efgsrel  19656  efgsp1  19659  frgpup1  19697  rnghmmul  20377  c0snmgmhm  20390  zrrnghm  20461  abvmul  20746  abvtri  20747  issrngd  20780  lmhmlin  20979  ipcj  21581  psrmulval  21891  mhpmulcl  22074  psdcoef  22085  psdadd  22088  psdpw  22095  coe1mul2  22193  coe1tmmul2fv  22202  coe1pwmulfv  22204  cply1mul  22221  mat1scmat  22464  mdetmul  22548  madufval  22562  cramer0  22615  cpmatmcllem  22643  d1mat2pmat  22664  m2cpminvid2lem  22679  decpmatmullem  22696  decpmatmulsumfsupp  22698  pm2mpmhmlem1  22743  pm2mpmhmlem2  22744  cayhamlem1  22791  cpmadumatpoly  22808  cayleyhamilton  22815  1stcelcls  23386  imasdsf1olem  24298  comet  24438  nrmmetd  24499  tngngp  24579  tngngp3  24581  nmvs  24601  mulc1cncf  24835  cncfco  24837  pi1xfr  24992  pi1coghm  24998  caubl  25245  caublcls  25246  bcthlem2  25262  bcthlem3  25263  bcthlem4  25264  bcthlem5  25265  ivthlem2  25390  ovolicc2lem4  25458  volsuplem  25493  volsup  25494  uniioombllem3  25523  itg1climres  25652  itg2monolem1  25688  itg2i1fseqle  25692  itg2i1fseq  25693  itg2i1fseq2  25694  itg2addlem  25696  itgeq2  25716  dvferm1lem  25925  dvferm2lem  25927  dvlip  25935  c1lip1  25939  lhop1lem  25955  lhop1  25956  ftc1lem4  25983  ftc1lem6  25985  mdegmullem  26020  coe1mul3  26041  ply1divex  26079  coeeu  26167  coeeq  26169  coemullem  26192  coemul  26194  dvply1  26228  dvply2g  26229  dvply2gOLD  26230  aalioulem3  26279  aaliou3lem8  26290  ulmshftlem  26335  ulmshft  26336  ulmss  26343  pserdvlem2  26375  cxpcn3lem  26694  loglesqrt  26708  birthdaylem2  26899  emcllem2  26944  emcllem3  26945  harmonicbnd2  26952  lgamgulmlem2  26977  lgamgulmlem3  26978  lgamgulmlem5  26980  lgambdd  26984  lgamcvglem  26987  facgam  27013  ftalem7  27026  bposlem7  27238  bposlem9  27240  lgsqrlem2  27295  lgsqrlem4  27297  2lgslem3a  27344  2lgslem3b  27345  2lgslem3c  27346  2lgslem3d  27347  rplogsumlem1  27432  dchrvmasumlem1  27443  logsqvma  27490  logsqvma2  27491  selberglem3  27495  selberg  27496  selberg2lem  27498  selberg4lem1  27508  pntrsumo1  27513  selberg34r  27519  pntsval  27520  pntsval2  27524  pntrlog2bndlem1  27525  pntrlog2bndlem4  27528  pntpbnd  27536  pntibnd  27541  pntlemo  27555  addsbday  27970  seqsval  28228  seqsp1  28251  zs12bday  28404  ewlkinedg  29594  wkslem1  29597  uspgr2wlkeq  29635  wlkdlem2  29671  upgrwlkdvdelem  29725  crctcshwlkn0lem2  29800  crctcshwlkn0lem3  29801  crctcshwlkn0lem4  29802  crctcshwlkn0lem5  29803  wlkiswwlks2lem2  29859  wlkiswwlks2lem5  29862  wwlksnext  29882  wwlksnredwwlkn  29884  wwlksnextproplem2  29899  clwwlkccatlem  29980  clwlkclwwlklem2a1  29983  clwlkclwwlklem2fv1  29986  clwlkclwwlklem2a4  29988  clwlkclwwlklem2a  29989  clwlkclwwlklem2  29991  clwwisshclwwslemlem  30004  clwwisshclwws  30006  clwwlknlbonbgr1  30030  clwwlkel  30037  clwwlkf  30038  clwwlkwwlksb  30045  clwwlkext2edg  30047  wwlksext2clwwlk  30048  clwwlknonex2lem2  30099  eupthseg  30197  upgreupthseg  30200  eupth2lem3  30227  2clwwlk2clwwlklem  30337  2clwwlk  30338  numclwwlk1lem2f1  30348  numclwlk1lem2  30361  nvs  30654  nvtri  30661  ipval  30694  blocnilem  30795  phpar2  30814  phpar  30815  sii  30845  normsub0  31127  norm-ii  31129  norm-iii  31131  normsub  31134  normpyth  31136  norm3dif  31141  norm3lemt  31143  norm3adifi  31144  normpar  31146  polid  31150  bcs  31172  pjaddi  31677  pjsubi  31679  pjmuli  31680  pjcjt2  31683  lnopeq0lem2  31997  lnopunilem2  32002  branmfn  32096  hstel2  32210  stj  32226  cdj3lem1  32425  cdj3lem2b  32428  cdj3lem3b  32431  cdj3i  32432  ccatws1f1o  32943  elrgspnlem2  33221  constrsuc  33762  cnre2csqlem  33934  cnre2csqima  33935  mndpluscn  33950  lmdvg  33977  plymulx  34572  signsvfn  34606  subfacval2  35242  cvmliftlem7  35346  elmrsubrn  35575  faclim2  35803  fwddifval  36217  fwddifnval  36218  dnival  36526  unblimceq0lem  36561  unbdqndv2  36566  matunitlindf  37668  poimirlem32  37702  itg2gt0cn  37725  ftc1cnnclem  37741  ftc1cnnc  37742  areacirc  37763  sdclem1  37793  fdc  37795  seqpo  37797  incsequz  37798  incsequz2  37799  mettrifi  37807  caushft  37811  bfplem1  37872  ghomco  37941  rngohomadd  38019  rngohommul  38020  dihval  41341  lclkrlem1  41615  hdmap14lem2a  41976  hgmapval  41996  deg1pow  42244  sticksstones10  42258  sticksstones12a  42260  abvexp  42640  fsuppind  42698  prjspnval  42724  incssnn0  42818  rencldnfilem  42927  irrapxlem5  42933  irrapxlem6  42934  pellexlem3  42938  cvgdvgrat  44420  radcnvrat  44421  hashnzfzclim  44429  binomcxplemradcnv  44459  iunincfi  45205  monoords  45412  fperiodmullem  45418  monoordxrv  45593  monoordxr  45594  monoord2xrv  45595  monoord2xr  45596  climinf  45720  climsuse  45722  climinff  45725  mullimc  45730  mullimcf  45737  idlimc  45740  limcperiod  45742  limcrecl  45743  limclner  45763  climinf2  45819  climxrrelem  45861  cnrefiisplem  45941  cnrefiisp  45942  climxlim2lem  45957  cncfshift  45986  cncfperiod  45991  fperdvper  46031  dvnmul  46055  iblspltprt  46085  itgspltprt  46091  itgiccshift  46092  itgperiod  46093  dirkerval2  46206  dirkertrigeqlem1  46210  dirkertrigeqlem2  46211  dirkertrigeqlem3  46212  dirkercncflem2  46216  dirkercncflem3  46217  fourierdlem29  46248  elaa2lem  46345  elaa2  46346  nnfoctbdj  46568  meaiuninclem  46592  meaiunincf  46595  meaiuninc3v  46596  meaiuninc3  46597  meaiininclem  46598  meaiininc  46599  smflimlem6  46888  ormkglobd  46987  natglobalincr  46989  2ltceilhalf  47442  ceilhalfnn  47450  smonoord  47485  iccpartimp  47531  iccelpart  47547  icceuelpart  47550  fargshiftfv  47553  fmtnorec2  47657  bgoldbtbndlem2  47920  bgoldbtbndlem3  47921  bgoldbtbnd  47923  upgrimwlklem5  48015  gpgov  48156  gpg5nbgrvtx13starlem2  48186  ply1mulgsumlem3  48503  ply1mulgsumlem4  48504  ply1mulgsum  48505  ackvalsuc1  48794