Theorem fvoveq1 7206

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

Syntax hints:   → wi 4   = wceq 1542  ‘cfv 6350  (class class class)co 7183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-v 3402  df-un 3858  df-in 3860  df-ss 3870  df-sn 4527  df-pr 4529  df-op 4533  df-uni 4807  df-br 5041  df-iota 6308  df-fv 6358  df-ov 7186

This theorem is referenced by:  eluzadd  12368  eluzsub  12369  fldiv4p1lem1div2  13309  fldiv4lem1div2  13311  modval  13343  seqval  13484  seqp1  13488  seqshft2  13501  monoord  13505  monoord2  13506  seqhomo  13522  facp1  13743  faclbnd4lem2  13759  bcval  13769  lsw0  14019  ccatval1  14032  ccatval1OLD  14033  ccatval2  14034  ccatalpha  14049  swrdfv  14112  2swrd2eqwrdeq  14417  imval  14569  recan  14799  rlimcld2  15038  rlimcn1  15048  rlimcn3  15050  climcn1  15052  climcn2  15053  subcn2  15055  o1of2  15073  isercoll2  15131  climsup  15132  serf0  15143  iseraltlem2  15145  fsumrelem  15268  mertenslem1  15345  mertenslem2  15346  mertens  15347  bitsfval  15879  smuval  15937  pcfac  16348  vdwlem6  16435  vdwlem8  16437  vdwlem9  16438  vdwlem10  16439  imasaddvallem  16918  imasvscafn  16926  imasvscaval  16927  mhmlin  18092  mhmlem  18350  mulginvcom  18383  mhmmulg  18399  ghmlin  18494  efgsdm  18987  efgsdmi  18989  efgsrel  18991  efgsp1  18994  frgpup1  19032  abvmul  19732  abvtri  19733  issrngd  19764  lmhmlin  19939  ipcj  20463  psrmulval  20778  mhpmulcl  20956  coe1mul2  21057  coe1tmmul2fv  21066  coe1pwmulfv  21068  cply1mul  21082  mat1scmat  21303  mdetmul  21387  madufval  21401  cramer0  21454  cpmatmcllem  21482  d1mat2pmat  21503  m2cpminvid2lem  21518  decpmatmullem  21535  decpmatmulsumfsupp  21537  pm2mpmhmlem1  21582  pm2mpmhmlem2  21583  cayhamlem1  21630  cpmadumatpoly  21647  cayleyhamilton  21654  1stcelcls  22225  imasdsf1olem  23139  comet  23279  nrmmetd  23340  tngngp  23420  tngngp3  23422  nmvs  23442  mulc1cncf  23670  cncfco  23672  pi1xfr  23820  pi1coghm  23826  caubl  24073  caublcls  24074  bcthlem2  24090  bcthlem3  24091  bcthlem4  24092  bcthlem5  24093  ivthlem2  24217  ovolicc2lem4  24285  volsuplem  24320  volsup  24321  uniioombllem3  24350  itg1climres  24480  itg2monolem1  24516  itg2i1fseqle  24520  itg2i1fseq  24521  itg2i1fseq2  24522  itg2addlem  24524  itgeq2  24543  dvferm1lem  24749  dvferm2lem  24751  dvlip  24758  c1lip1  24762  lhop1lem  24778  lhop1  24779  ftc1lem4  24804  ftc1lem6  24806  mdegmullem  24844  coe1mul3  24865  ply1divex  24902  coeeu  24987  coeeq  24989  coemullem  25012  coemul  25014  dvply1  25045  dvply2g  25046  aalioulem3  25095  aaliou3lem8  25106  ulmshftlem  25149  ulmshft  25150  ulmss  25157  pserdvlem2  25188  cxpcn3lem  25501  loglesqrt  25512  birthdaylem2  25703  emcllem2  25747  emcllem3  25748  harmonicbnd2  25755  lgamgulmlem2  25780  lgamgulmlem3  25781  lgamgulmlem5  25783  lgambdd  25787  lgamcvglem  25790  facgam  25816  ftalem7  25829  bposlem7  26039  bposlem9  26041  lgsqrlem2  26096  lgsqrlem4  26098  2lgslem3a  26145  2lgslem3b  26146  2lgslem3c  26147  2lgslem3d  26148  rplogsumlem1  26233  dchrvmasumlem1  26244  logsqvma  26291  logsqvma2  26292  selberglem3  26296  selberg  26297  selberg2lem  26299  selberg4lem1  26309  pntrsumo1  26314  selberg34r  26320  pntsval  26321  pntsval2  26325  pntrlog2bndlem1  26326  pntrlog2bndlem4  26329  pntpbnd  26337  pntibnd  26342  pntlemo  26356  ewlkinedg  27559  wkslem1  27562  uspgr2wlkeq  27600  wlkdlem2  27638  upgrwlkdvdelem  27690  crctcshwlkn0lem2  27762  crctcshwlkn0lem3  27763  crctcshwlkn0lem4  27764  crctcshwlkn0lem5  27765  wlkiswwlks2lem2  27821  wlkiswwlks2lem5  27824  wwlksnext  27844  wwlksnredwwlkn  27846  wwlksnextproplem2  27861  clwwlkccatlem  27939  clwlkclwwlklem2a1  27942  clwlkclwwlklem2fv1  27945  clwlkclwwlklem2a4  27947  clwlkclwwlklem2a  27948  clwlkclwwlklem2  27950  clwwisshclwwslemlem  27963  clwwisshclwws  27965  clwwlknlbonbgr1  27989  clwwlkel  27996  clwwlkf  27997  clwwlkwwlksb  28004  clwwlkext2edg  28006  wwlksext2clwwlk  28007  clwwlknonex2lem2  28058  eupthseg  28156  upgreupthseg  28159  eupth2lem3  28186  2clwwlk2clwwlklem  28296  2clwwlk  28297  numclwwlk1lem2f1  28307  numclwlk1lem2  28320  nvs  28611  nvtri  28618  ipval  28651  blocnilem  28752  phpar2  28771  phpar  28772  sii  28802  normsub0  29084  norm-ii  29086  norm-iii  29088  normsub  29091  normpyth  29093  norm3dif  29098  norm3lemt  29100  norm3adifi  29101  normpar  29103  polid  29107  bcs  29129  pjaddi  29634  pjsubi  29636  pjmuli  29637  pjcjt2  29640  lnopeq0lem2  29954  lnopunilem2  29959  branmfn  30053  hstel2  30167  stj  30183  cdj3lem1  30382  cdj3lem2b  30385  cdj3lem3b  30388  cdj3i  30389  cnre2csqlem  31445  cnre2csqima  31446  mndpluscn  31461  lmdvg  31488  plymulx  32110  signsvfn  32144  subfacval2  32733  cvmliftlem7  32837  elmrsubrn  33066  faclim2  33300  fwddifval  34120  fwddifnval  34121  dnival  34307  unblimceq0lem  34342  unbdqndv2  34347  matunitlindf  35431  poimirlem32  35465  itg2gt0cn  35488  ftc1cnnclem  35504  ftc1cnnc  35505  areacirc  35526  sdclem1  35557  fdc  35559  seqpo  35561  incsequz  35562  incsequz2  35563  mettrifi  35571  caushft  35575  bfplem1  35636  ghomco  35705  rngohomadd  35783  rngohommul  35784  dihval  38902  lclkrlem1  39176  hdmap14lem2a  39537  hgmapval  39557  sticksstones10  39750  sticksstones12a  39752  fsuppind  39899  prjspnval  40073  incssnn0  40146  rencldnfilem  40255  irrapxlem5  40261  irrapxlem6  40262  pellexlem3  40266  cvgdvgrat  41510  radcnvrat  41511  hashnzfzclim  41519  binomcxplemradcnv  41549  iunincfi  42223  monoords  42415  fperiodmullem  42421  monoordxrv  42603  monoordxr  42604  monoord2xrv  42605  monoord2xr  42606  climinf  42730  climsuse  42732  climinff  42735  mullimc  42740  mullimcf  42747  idlimc  42750  limcperiod  42752  limcrecl  42753  limclner  42775  climinf2  42831  climxrrelem  42873  cnrefiisplem  42953  cnrefiisp  42954  climxlim2lem  42969  cncfshift  42998  cncfperiod  43003  fperdvper  43043  dvnmul  43067  iblspltprt  43097  itgspltprt  43103  itgiccshift  43104  itgperiod  43105  dirkerval2  43218  dirkertrigeqlem1  43222  dirkertrigeqlem2  43223  dirkertrigeqlem3  43224  dirkercncflem2  43228  dirkercncflem3  43229  fourierdlem29  43260  elaa2lem  43357  elaa2  43358  nnfoctbdj  43577  meaiuninclem  43601  meaiunincf  43604  meaiuninc3v  43605  meaiuninc3  43606  meaiininclem  43607  meaiininc  43608  smflimlem6  43891  smonoord  44405  iccpartimp  44451  iccelpart  44467  icceuelpart  44470  fargshiftfv  44473  fmtnorec2  44577  bgoldbtbndlem2  44840  bgoldbtbndlem3  44841  bgoldbtbnd  44843  mgmhmlin  44922  rnghmmul  45040  c0snmgmhm  45054  zrrnghm  45057  ply1mulgsumlem3  45311  ply1mulgsumlem4  45312  ply1mulgsum  45313  ackvalsuc1  45607