Theorem fvoveq1 7372

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

Syntax hints:   → wi 4   = wceq 1540  ‘cfv 6482  (class class class)co 7349

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352

This theorem is referenced by:  coof  7637  eluzaddOLD  12770  eluzsubOLD  12771  fldiv4p1lem1div2  13739  fldiv4lem1div2  13741  modval  13775  seqval  13919  seqp1  13923  seqshft2  13935  monoord  13939  monoord2  13940  seqhomo  13956  facp1  14185  faclbnd4lem2  14201  bcval  14211  lsw0  14472  ccatval1  14484  ccatval2  14485  ccatalpha  14500  swrdfv  14555  2swrd2eqwrdeq  14860  imval  15014  recan  15244  rlimcld2  15485  rlimcn1  15495  rlimcn3  15497  climcn1  15499  climcn2  15500  subcn2  15502  o1of2  15520  isercoll2  15576  climsup  15577  serf0  15588  iseraltlem2  15590  fsumrelem  15714  mertenslem1  15791  mertenslem2  15792  mertens  15793  bitsfval  16334  smuval  16392  pcfac  16811  vdwlem6  16898  vdwlem8  16900  vdwlem9  16901  vdwlem10  16902  imasaddvallem  17433  imasvscafn  17441  imasvscaval  17442  mgmhmlin  18573  mhmlin  18667  mhmlem  18941  mulginvcom  18978  mhmmulg  18994  ghmlin  19100  efgsdm  19609  efgsdmi  19611  efgsrel  19613  efgsp1  19616  frgpup1  19654  rnghmmul  20334  c0snmgmhm  20347  zrrnghm  20421  abvmul  20706  abvtri  20707  issrngd  20740  lmhmlin  20939  ipcj  21541  psrmulval  21851  mhpmulcl  22034  psdcoef  22045  psdadd  22048  psdpw  22055  coe1mul2  22153  coe1tmmul2fv  22162  coe1pwmulfv  22164  cply1mul  22181  mat1scmat  22424  mdetmul  22508  madufval  22522  cramer0  22575  cpmatmcllem  22603  d1mat2pmat  22624  m2cpminvid2lem  22639  decpmatmullem  22656  decpmatmulsumfsupp  22658  pm2mpmhmlem1  22703  pm2mpmhmlem2  22704  cayhamlem1  22751  cpmadumatpoly  22768  cayleyhamilton  22775  1stcelcls  23346  imasdsf1olem  24259  comet  24399  nrmmetd  24460  tngngp  24540  tngngp3  24542  nmvs  24562  mulc1cncf  24796  cncfco  24798  pi1xfr  24953  pi1coghm  24959  caubl  25206  caublcls  25207  bcthlem2  25223  bcthlem3  25224  bcthlem4  25225  bcthlem5  25226  ivthlem2  25351  ovolicc2lem4  25419  volsuplem  25454  volsup  25455  uniioombllem3  25484  itg1climres  25613  itg2monolem1  25649  itg2i1fseqle  25653  itg2i1fseq  25654  itg2i1fseq2  25655  itg2addlem  25657  itgeq2  25677  dvferm1lem  25886  dvferm2lem  25888  dvlip  25896  c1lip1  25900  lhop1lem  25916  lhop1  25917  ftc1lem4  25944  ftc1lem6  25946  mdegmullem  25981  coe1mul3  26002  ply1divex  26040  coeeu  26128  coeeq  26130  coemullem  26153  coemul  26155  dvply1  26189  dvply2g  26190  dvply2gOLD  26191  aalioulem3  26240  aaliou3lem8  26251  ulmshftlem  26296  ulmshft  26297  ulmss  26304  pserdvlem2  26336  cxpcn3lem  26655  loglesqrt  26669  birthdaylem2  26860  emcllem2  26905  emcllem3  26906  harmonicbnd2  26913  lgamgulmlem2  26938  lgamgulmlem3  26939  lgamgulmlem5  26941  lgambdd  26945  lgamcvglem  26948  facgam  26974  ftalem7  26987  bposlem7  27199  bposlem9  27201  lgsqrlem2  27256  lgsqrlem4  27258  2lgslem3a  27305  2lgslem3b  27306  2lgslem3c  27307  2lgslem3d  27308  rplogsumlem1  27393  dchrvmasumlem1  27404  logsqvma  27451  logsqvma2  27452  selberglem3  27456  selberg  27457  selberg2lem  27459  selberg4lem1  27469  pntrsumo1  27474  selberg34r  27480  pntsval  27481  pntsval2  27485  pntrlog2bndlem1  27486  pntrlog2bndlem4  27489  pntpbnd  27497  pntibnd  27502  pntlemo  27516  addsbday  27929  seqsval  28187  seqsp1  28210  zs12bday  28361  ewlkinedg  29550  wkslem1  29553  uspgr2wlkeq  29591  wlkdlem2  29627  upgrwlkdvdelem  29681  crctcshwlkn0lem2  29756  crctcshwlkn0lem3  29757  crctcshwlkn0lem4  29758  crctcshwlkn0lem5  29759  wlkiswwlks2lem2  29815  wlkiswwlks2lem5  29818  wwlksnext  29838  wwlksnredwwlkn  29840  wwlksnextproplem2  29855  clwwlkccatlem  29933  clwlkclwwlklem2a1  29936  clwlkclwwlklem2fv1  29939  clwlkclwwlklem2a4  29941  clwlkclwwlklem2a  29942  clwlkclwwlklem2  29944  clwwisshclwwslemlem  29957  clwwisshclwws  29959  clwwlknlbonbgr1  29983  clwwlkel  29990  clwwlkf  29991  clwwlkwwlksb  29998  clwwlkext2edg  30000  wwlksext2clwwlk  30001  clwwlknonex2lem2  30052  eupthseg  30150  upgreupthseg  30153  eupth2lem3  30180  2clwwlk2clwwlklem  30290  2clwwlk  30291  numclwwlk1lem2f1  30301  numclwlk1lem2  30314  nvs  30607  nvtri  30614  ipval  30647  blocnilem  30748  phpar2  30767  phpar  30768  sii  30798  normsub0  31080  norm-ii  31082  norm-iii  31084  normsub  31087  normpyth  31089  norm3dif  31094  norm3lemt  31096  norm3adifi  31097  normpar  31099  polid  31103  bcs  31125  pjaddi  31630  pjsubi  31632  pjmuli  31633  pjcjt2  31636  lnopeq0lem2  31950  lnopunilem2  31955  branmfn  32049  hstel2  32163  stj  32179  cdj3lem1  32378  cdj3lem2b  32381  cdj3lem3b  32384  cdj3i  32385  ccatws1f1o  32893  chnltm1  32950  chnind  32953  elrgspnlem2  33183  constrsuc  33705  cnre2csqlem  33877  cnre2csqima  33878  mndpluscn  33893  lmdvg  33920  plymulx  34516  signsvfn  34550  subfacval2  35164  cvmliftlem7  35268  elmrsubrn  35497  faclim2  35725  fwddifval  36140  fwddifnval  36141  dnival  36449  unblimceq0lem  36484  unbdqndv2  36489  matunitlindf  37602  poimirlem32  37636  itg2gt0cn  37659  ftc1cnnclem  37675  ftc1cnnc  37676  areacirc  37697  sdclem1  37727  fdc  37729  seqpo  37731  incsequz  37732  incsequz2  37733  mettrifi  37741  caushft  37745  bfplem1  37806  ghomco  37875  rngohomadd  37953  rngohommul  37954  dihval  41215  lclkrlem1  41489  hdmap14lem2a  41850  hgmapval  41870  deg1pow  42118  sticksstones10  42132  sticksstones12a  42134  abvexp  42509  fsuppind  42567  prjspnval  42593  incssnn0  42688  rencldnfilem  42797  irrapxlem5  42803  irrapxlem6  42804  pellexlem3  42808  cvgdvgrat  44290  radcnvrat  44291  hashnzfzclim  44299  binomcxplemradcnv  44329  iunincfi  45076  monoords  45283  fperiodmullem  45289  monoordxrv  45464  monoordxr  45465  monoord2xrv  45466  monoord2xr  45467  climinf  45591  climsuse  45593  climinff  45596  mullimc  45601  mullimcf  45608  idlimc  45611  limcperiod  45613  limcrecl  45614  limclner  45636  climinf2  45692  climxrrelem  45734  cnrefiisplem  45814  cnrefiisp  45815  climxlim2lem  45830  cncfshift  45859  cncfperiod  45864  fperdvper  45904  dvnmul  45928  iblspltprt  45958  itgspltprt  45964  itgiccshift  45965  itgperiod  45966  dirkerval2  46079  dirkertrigeqlem1  46083  dirkertrigeqlem2  46084  dirkertrigeqlem3  46085  dirkercncflem2  46089  dirkercncflem3  46090  fourierdlem29  46121  elaa2lem  46218  elaa2  46219  nnfoctbdj  46441  meaiuninclem  46465  meaiunincf  46468  meaiuninc3v  46469  meaiuninc3  46470  meaiininclem  46471  meaiininc  46472  smflimlem6  46761  ormkglobd  46860  natglobalincr  46862  tworepnotupword  46871  2ltceilhalf  47316  ceilhalfnn  47324  smonoord  47359  iccpartimp  47405  iccelpart  47421  icceuelpart  47424  fargshiftfv  47427  fmtnorec2  47531  bgoldbtbndlem2  47794  bgoldbtbndlem3  47795  bgoldbtbnd  47797  upgrimwlklem5  47889  gpgov  48030  gpg5nbgrvtx13starlem2  48060  ply1mulgsumlem3  48377  ply1mulgsumlem4  48378  ply1mulgsum  48379  ackvalsuc1  48668