Theorem fvoveq1 7384

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

Syntax hints:   → wi 4   = wceq 1542  ‘cfv 6493  (class class class)co 7361

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6449  df-fv 6501  df-ov 7364

This theorem is referenced by:  coof  7649  fldiv4p1lem1div2  13788  fldiv4lem1div2  13790  modval  13824  seqval  13968  seqp1  13972  seqshft2  13984  monoord  13988  monoord2  13989  seqhomo  14005  facp1  14234  faclbnd4lem2  14250  bcval  14260  lsw0  14521  ccatval1  14533  ccatval2  14534  ccatalpha  14550  swrdfv  14605  2swrd2eqwrdeq  14909  imval  15063  recan  15293  rlimcld2  15534  rlimcn1  15544  rlimcn3  15546  climcn1  15548  climcn2  15549  subcn2  15551  o1of2  15569  isercoll2  15625  climsup  15626  serf0  15637  iseraltlem2  15639  fsumrelem  15764  mertenslem1  15843  mertenslem2  15844  mertens  15845  bitsfval  16386  smuval  16444  pcfac  16864  vdwlem6  16951  vdwlem8  16953  vdwlem9  16954  vdwlem10  16955  imasaddvallem  17487  imasvscafn  17495  imasvscaval  17496  chnltm1  18569  chnind  18581  mgmhmlin  18661  mhmlin  18755  mhmlem  19032  mulginvcom  19069  mhmmulg  19085  ghmlin  19190  efgsdm  19699  efgsdmi  19701  efgsrel  19703  efgsp1  19706  frgpup1  19744  rnghmmul  20423  c0snmgmhm  20436  zrrnghm  20507  abvmul  20792  abvtri  20793  issrngd  20826  lmhmlin  21025  ipcj  21627  psrmulval  21936  mhpmulcl  22128  psdcoef  22139  psdadd  22142  psdpw  22149  coe1mul2  22247  coe1tmmul2fv  22256  coe1pwmulfv  22258  cply1mul  22274  mat1scmat  22517  mdetmul  22601  madufval  22615  cramer0  22668  cpmatmcllem  22696  d1mat2pmat  22717  m2cpminvid2lem  22732  decpmatmullem  22749  decpmatmulsumfsupp  22751  pm2mpmhmlem1  22796  pm2mpmhmlem2  22797  cayhamlem1  22844  cpmadumatpoly  22861  cayleyhamilton  22868  1stcelcls  23439  imasdsf1olem  24351  comet  24491  nrmmetd  24552  tngngp  24632  tngngp3  24634  nmvs  24654  mulc1cncf  24885  cncfco  24887  pi1xfr  25035  pi1coghm  25041  caubl  25288  caublcls  25289  bcthlem2  25305  bcthlem3  25306  bcthlem4  25307  bcthlem5  25308  ivthlem2  25432  ovolicc2lem4  25500  volsuplem  25535  volsup  25536  uniioombllem3  25565  itg1climres  25694  itg2monolem1  25730  itg2i1fseqle  25734  itg2i1fseq  25735  itg2i1fseq2  25736  itg2addlem  25738  itgeq2  25758  dvferm1lem  25964  dvferm2lem  25966  dvlip  25973  c1lip1  25977  lhop1lem  25993  lhop1  25994  ftc1lem4  26019  ftc1lem6  26021  mdegmullem  26056  coe1mul3  26077  ply1divex  26115  coeeu  26203  coeeq  26205  coemullem  26228  coemul  26230  dvply1  26263  dvply2g  26264  dvply2gOLD  26265  aalioulem3  26314  aaliou3lem8  26325  ulmshftlem  26370  ulmshft  26371  ulmss  26378  pserdvlem2  26409  cxpcn3lem  26727  loglesqrt  26741  birthdaylem2  26932  emcllem2  26977  emcllem3  26978  harmonicbnd2  26985  lgamgulmlem2  27010  lgamgulmlem3  27011  lgamgulmlem5  27013  lgambdd  27017  lgamcvglem  27020  facgam  27046  ftalem7  27059  bposlem7  27270  bposlem9  27272  lgsqrlem2  27327  lgsqrlem4  27329  2lgslem3a  27376  2lgslem3b  27377  2lgslem3c  27378  2lgslem3d  27379  rplogsumlem1  27464  dchrvmasumlem1  27475  logsqvma  27522  logsqvma2  27523  selberglem3  27527  selberg  27528  selberg2lem  27530  selberg4lem1  27540  pntrsumo1  27545  selberg34r  27551  pntsval  27552  pntsval2  27556  pntrlog2bndlem1  27557  pntrlog2bndlem4  27560  pntpbnd  27568  pntibnd  27573  pntlemo  27587  addbday  28027  addonbday  28288  seqsval  28297  seqsp1  28320  bdaypw2n0bndlem  28472  ewlkinedg  29691  wkslem1  29694  uspgr2wlkeq  29732  wlkdlem2  29768  upgrwlkdvdelem  29822  crctcshwlkn0lem2  29897  crctcshwlkn0lem3  29898  crctcshwlkn0lem4  29899  crctcshwlkn0lem5  29900  wlkiswwlks2lem2  29956  wlkiswwlks2lem5  29959  wwlksnext  29979  wwlksnredwwlkn  29981  wwlksnextproplem2  29996  clwwlkccatlem  30077  clwlkclwwlklem2a1  30080  clwlkclwwlklem2fv1  30083  clwlkclwwlklem2a4  30085  clwlkclwwlklem2a  30086  clwlkclwwlklem2  30088  clwwisshclwwslemlem  30101  clwwisshclwws  30103  clwwlknlbonbgr1  30127  clwwlkel  30134  clwwlkf  30135  clwwlkwwlksb  30142  clwwlkext2edg  30144  wwlksext2clwwlk  30145  clwwlknonex2lem2  30196  eupthseg  30294  upgreupthseg  30297  eupth2lem3  30324  2clwwlk2clwwlklem  30434  2clwwlk  30435  numclwwlk1lem2f1  30445  numclwlk1lem2  30458  nvs  30752  nvtri  30759  ipval  30792  blocnilem  30893  phpar2  30912  phpar  30913  sii  30943  normsub0  31225  norm-ii  31227  norm-iii  31229  normsub  31232  normpyth  31234  norm3dif  31239  norm3lemt  31241  norm3adifi  31242  normpar  31244  polid  31248  bcs  31270  pjaddi  31775  pjsubi  31777  pjmuli  31778  pjcjt2  31781  lnopeq0lem2  32095  lnopunilem2  32100  branmfn  32194  hstel2  32308  stj  32324  cdj3lem1  32523  cdj3lem2b  32526  cdj3lem3b  32529  cdj3i  32530  ccatws1f1o  33029  gsummulsubdishift1  33147  elrgspnlem2  33322  constrsuc  33901  cnre2csqlem  34073  cnre2csqima  34074  mndpluscn  34089  lmdvg  34116  plymulx  34711  signsvfn  34745  subfacval2  35388  cvmliftlem7  35492  elmrsubrn  35721  faclim2  35949  fwddifval  36363  fwddifnval  36364  dnival  36750  unblimceq0lem  36785  unbdqndv2  36790  matunitlindf  37956  poimirlem32  37990  itg2gt0cn  38013  ftc1cnnclem  38029  ftc1cnnc  38030  areacirc  38051  sdclem1  38081  fdc  38083  seqpo  38085  incsequz  38086  incsequz2  38087  mettrifi  38095  caushft  38099  bfplem1  38160  ghomco  38229  rngohomadd  38307  rngohommul  38308  dihval  41695  lclkrlem1  41969  hdmap14lem2a  42330  hgmapval  42350  deg1pow  42597  sticksstones10  42611  sticksstones12a  42613  abvexp  42994  fsuppind  43040  prjspnval  43066  incssnn0  43160  rencldnfilem  43269  irrapxlem5  43275  irrapxlem6  43276  pellexlem3  43280  cvgdvgrat  44761  radcnvrat  44762  hashnzfzclim  44770  binomcxplemradcnv  44800  iunincfi  45545  monoords  45751  fperiodmullem  45757  monoordxrv  45930  monoordxr  45931  monoord2xrv  45932  monoord2xr  45933  climinf  46057  climsuse  46059  climinff  46062  mullimc  46067  mullimcf  46074  idlimc  46077  limcperiod  46079  limcrecl  46080  limclner  46100  climinf2  46156  climxrrelem  46198  cnrefiisplem  46278  cnrefiisp  46279  climxlim2lem  46294  cncfshift  46323  cncfperiod  46328  fperdvper  46368  dvnmul  46392  iblspltprt  46422  itgspltprt  46428  itgiccshift  46429  itgperiod  46430  dirkerval2  46543  dirkertrigeqlem1  46547  dirkertrigeqlem2  46548  dirkertrigeqlem3  46549  dirkercncflem2  46553  dirkercncflem3  46554  fourierdlem29  46585  elaa2lem  46682  elaa2  46683  nnfoctbdj  46905  meaiuninclem  46929  meaiunincf  46932  meaiuninc3v  46933  meaiuninc3  46934  meaiininclem  46935  meaiininc  46936  smflimlem6  47225  ormkglobd  47324  natglobalincr  47326  2ltceilhalf  47795  ceilhalfnn  47803  smonoord  47840  iccpartimp  47892  iccelpart  47908  icceuelpart  47911  fargshiftfv  47914  fmtnorec2  48021  ppivalnnnprmge6  48104  ppivalnnnprm  48106  ppivalnn  48110  bgoldbtbndlem2  48297  bgoldbtbndlem3  48298  bgoldbtbnd  48300  upgrimwlklem5  48392  gpgov  48533  gpg5nbgrvtx13starlem2  48563  ply1mulgsumlem3  48879  ply1mulgsumlem4  48880  ply1mulgsum  48881  ackvalsuc1  49170