Theorem fvoveq1 7413

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

Syntax hints:   → wi 4   = wceq 1540  ‘cfv 6514  (class class class)co 7390

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393

This theorem is referenced by:  coof  7680  eluzaddOLD  12835  eluzsubOLD  12836  fldiv4p1lem1div2  13804  fldiv4lem1div2  13806  modval  13840  seqval  13984  seqp1  13988  seqshft2  14000  monoord  14004  monoord2  14005  seqhomo  14021  facp1  14250  faclbnd4lem2  14266  bcval  14276  lsw0  14537  ccatval1  14549  ccatval2  14550  ccatalpha  14565  swrdfv  14620  2swrd2eqwrdeq  14926  imval  15080  recan  15310  rlimcld2  15551  rlimcn1  15561  rlimcn3  15563  climcn1  15565  climcn2  15566  subcn2  15568  o1of2  15586  isercoll2  15642  climsup  15643  serf0  15654  iseraltlem2  15656  fsumrelem  15780  mertenslem1  15857  mertenslem2  15858  mertens  15859  bitsfval  16400  smuval  16458  pcfac  16877  vdwlem6  16964  vdwlem8  16966  vdwlem9  16967  vdwlem10  16968  imasaddvallem  17499  imasvscafn  17507  imasvscaval  17508  mgmhmlin  18633  mhmlin  18727  mhmlem  19001  mulginvcom  19038  mhmmulg  19054  ghmlin  19160  efgsdm  19667  efgsdmi  19669  efgsrel  19671  efgsp1  19674  frgpup1  19712  rnghmmul  20365  c0snmgmhm  20378  zrrnghm  20452  abvmul  20737  abvtri  20738  issrngd  20771  lmhmlin  20949  ipcj  21550  psrmulval  21860  mhpmulcl  22043  psdcoef  22054  psdadd  22057  psdpw  22064  coe1mul2  22162  coe1tmmul2fv  22171  coe1pwmulfv  22173  cply1mul  22190  mat1scmat  22433  mdetmul  22517  madufval  22531  cramer0  22584  cpmatmcllem  22612  d1mat2pmat  22633  m2cpminvid2lem  22648  decpmatmullem  22665  decpmatmulsumfsupp  22667  pm2mpmhmlem1  22712  pm2mpmhmlem2  22713  cayhamlem1  22760  cpmadumatpoly  22777  cayleyhamilton  22784  1stcelcls  23355  imasdsf1olem  24268  comet  24408  nrmmetd  24469  tngngp  24549  tngngp3  24551  nmvs  24571  mulc1cncf  24805  cncfco  24807  pi1xfr  24962  pi1coghm  24968  caubl  25215  caublcls  25216  bcthlem2  25232  bcthlem3  25233  bcthlem4  25234  bcthlem5  25235  ivthlem2  25360  ovolicc2lem4  25428  volsuplem  25463  volsup  25464  uniioombllem3  25493  itg1climres  25622  itg2monolem1  25658  itg2i1fseqle  25662  itg2i1fseq  25663  itg2i1fseq2  25664  itg2addlem  25666  itgeq2  25686  dvferm1lem  25895  dvferm2lem  25897  dvlip  25905  c1lip1  25909  lhop1lem  25925  lhop1  25926  ftc1lem4  25953  ftc1lem6  25955  mdegmullem  25990  coe1mul3  26011  ply1divex  26049  coeeu  26137  coeeq  26139  coemullem  26162  coemul  26164  dvply1  26198  dvply2g  26199  dvply2gOLD  26200  aalioulem3  26249  aaliou3lem8  26260  ulmshftlem  26305  ulmshft  26306  ulmss  26313  pserdvlem2  26345  cxpcn3lem  26664  loglesqrt  26678  birthdaylem2  26869  emcllem2  26914  emcllem3  26915  harmonicbnd2  26922  lgamgulmlem2  26947  lgamgulmlem3  26948  lgamgulmlem5  26950  lgambdd  26954  lgamcvglem  26957  facgam  26983  ftalem7  26996  bposlem7  27208  bposlem9  27210  lgsqrlem2  27265  lgsqrlem4  27267  2lgslem3a  27314  2lgslem3b  27315  2lgslem3c  27316  2lgslem3d  27317  rplogsumlem1  27402  dchrvmasumlem1  27413  logsqvma  27460  logsqvma2  27461  selberglem3  27465  selberg  27466  selberg2lem  27468  selberg4lem1  27478  pntrsumo1  27483  selberg34r  27489  pntsval  27490  pntsval2  27494  pntrlog2bndlem1  27495  pntrlog2bndlem4  27498  pntpbnd  27506  pntibnd  27511  pntlemo  27525  addsbday  27931  seqsval  28189  seqsp1  28212  zs12bday  28350  ewlkinedg  29539  wkslem1  29542  uspgr2wlkeq  29581  wlkdlem2  29618  upgrwlkdvdelem  29673  crctcshwlkn0lem2  29748  crctcshwlkn0lem3  29749  crctcshwlkn0lem4  29750  crctcshwlkn0lem5  29751  wlkiswwlks2lem2  29807  wlkiswwlks2lem5  29810  wwlksnext  29830  wwlksnredwwlkn  29832  wwlksnextproplem2  29847  clwwlkccatlem  29925  clwlkclwwlklem2a1  29928  clwlkclwwlklem2fv1  29931  clwlkclwwlklem2a4  29933  clwlkclwwlklem2a  29934  clwlkclwwlklem2  29936  clwwisshclwwslemlem  29949  clwwisshclwws  29951  clwwlknlbonbgr1  29975  clwwlkel  29982  clwwlkf  29983  clwwlkwwlksb  29990  clwwlkext2edg  29992  wwlksext2clwwlk  29993  clwwlknonex2lem2  30044  eupthseg  30142  upgreupthseg  30145  eupth2lem3  30172  2clwwlk2clwwlklem  30282  2clwwlk  30283  numclwwlk1lem2f1  30293  numclwlk1lem2  30306  nvs  30599  nvtri  30606  ipval  30639  blocnilem  30740  phpar2  30759  phpar  30760  sii  30790  normsub0  31072  norm-ii  31074  norm-iii  31076  normsub  31079  normpyth  31081  norm3dif  31086  norm3lemt  31088  norm3adifi  31089  normpar  31091  polid  31095  bcs  31117  pjaddi  31622  pjsubi  31624  pjmuli  31625  pjcjt2  31628  lnopeq0lem2  31942  lnopunilem2  31947  branmfn  32041  hstel2  32155  stj  32171  cdj3lem1  32370  cdj3lem2b  32373  cdj3lem3b  32376  cdj3i  32377  ccatws1f1o  32880  chnltm1  32941  chnind  32944  elrgspnlem2  33201  constrsuc  33735  cnre2csqlem  33907  cnre2csqima  33908  mndpluscn  33923  lmdvg  33950  plymulx  34546  signsvfn  34580  subfacval2  35181  cvmliftlem7  35285  elmrsubrn  35514  faclim2  35742  fwddifval  36157  fwddifnval  36158  dnival  36466  unblimceq0lem  36501  unbdqndv2  36506  matunitlindf  37619  poimirlem32  37653  itg2gt0cn  37676  ftc1cnnclem  37692  ftc1cnnc  37693  areacirc  37714  sdclem1  37744  fdc  37746  seqpo  37748  incsequz  37749  incsequz2  37750  mettrifi  37758  caushft  37762  bfplem1  37823  ghomco  37892  rngohomadd  37970  rngohommul  37971  dihval  41233  lclkrlem1  41507  hdmap14lem2a  41868  hgmapval  41888  deg1pow  42136  sticksstones10  42150  sticksstones12a  42152  abvexp  42527  fsuppind  42585  prjspnval  42611  incssnn0  42706  rencldnfilem  42815  irrapxlem5  42821  irrapxlem6  42822  pellexlem3  42826  cvgdvgrat  44309  radcnvrat  44310  hashnzfzclim  44318  binomcxplemradcnv  44348  iunincfi  45095  monoords  45302  fperiodmullem  45308  monoordxrv  45484  monoordxr  45485  monoord2xrv  45486  monoord2xr  45487  climinf  45611  climsuse  45613  climinff  45616  mullimc  45621  mullimcf  45628  idlimc  45631  limcperiod  45633  limcrecl  45634  limclner  45656  climinf2  45712  climxrrelem  45754  cnrefiisplem  45834  cnrefiisp  45835  climxlim2lem  45850  cncfshift  45879  cncfperiod  45884  fperdvper  45924  dvnmul  45948  iblspltprt  45978  itgspltprt  45984  itgiccshift  45985  itgperiod  45986  dirkerval2  46099  dirkertrigeqlem1  46103  dirkertrigeqlem2  46104  dirkertrigeqlem3  46105  dirkercncflem2  46109  dirkercncflem3  46110  fourierdlem29  46141  elaa2lem  46238  elaa2  46239  nnfoctbdj  46461  meaiuninclem  46485  meaiunincf  46488  meaiuninc3v  46489  meaiuninc3  46490  meaiininclem  46491  meaiininc  46492  smflimlem6  46781  ormkglobd  46880  natglobalincr  46882  tworepnotupword  46891  2ltceilhalf  47333  ceilhalfnn  47341  smonoord  47376  iccpartimp  47422  iccelpart  47438  icceuelpart  47441  fargshiftfv  47444  fmtnorec2  47548  bgoldbtbndlem2  47811  bgoldbtbndlem3  47812  bgoldbtbnd  47814  upgrimwlklem5  47905  gpgov  48037  gpg5nbgrvtx13starlem2  48067  ply1mulgsumlem3  48381  ply1mulgsumlem4  48382  ply1mulgsum  48383  ackvalsuc1  48672