Theorem fvoveq1 7381

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

Syntax hints:   → wi 4   = wceq 1541  ‘cfv 6492  (class class class)co 7358

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361

This theorem is referenced by:  coof  7646  fldiv4p1lem1div2  13755  fldiv4lem1div2  13757  modval  13791  seqval  13935  seqp1  13939  seqshft2  13951  monoord  13955  monoord2  13956  seqhomo  13972  facp1  14201  faclbnd4lem2  14217  bcval  14227  lsw0  14488  ccatval1  14500  ccatval2  14501  ccatalpha  14517  swrdfv  14572  2swrd2eqwrdeq  14876  imval  15030  recan  15260  rlimcld2  15501  rlimcn1  15511  rlimcn3  15513  climcn1  15515  climcn2  15516  subcn2  15518  o1of2  15536  isercoll2  15592  climsup  15593  serf0  15604  iseraltlem2  15606  fsumrelem  15730  mertenslem1  15807  mertenslem2  15808  mertens  15809  bitsfval  16350  smuval  16408  pcfac  16827  vdwlem6  16914  vdwlem8  16916  vdwlem9  16917  vdwlem10  16918  imasaddvallem  17450  imasvscafn  17458  imasvscaval  17459  chnltm1  18532  chnind  18544  mgmhmlin  18624  mhmlin  18718  mhmlem  18992  mulginvcom  19029  mhmmulg  19045  ghmlin  19150  efgsdm  19659  efgsdmi  19661  efgsrel  19663  efgsp1  19666  frgpup1  19704  rnghmmul  20385  c0snmgmhm  20398  zrrnghm  20469  abvmul  20754  abvtri  20755  issrngd  20788  lmhmlin  20987  ipcj  21589  psrmulval  21900  mhpmulcl  22092  psdcoef  22103  psdadd  22106  psdpw  22113  coe1mul2  22211  coe1tmmul2fv  22220  coe1pwmulfv  22222  cply1mul  22240  mat1scmat  22483  mdetmul  22567  madufval  22581  cramer0  22634  cpmatmcllem  22662  d1mat2pmat  22683  m2cpminvid2lem  22698  decpmatmullem  22715  decpmatmulsumfsupp  22717  pm2mpmhmlem1  22762  pm2mpmhmlem2  22763  cayhamlem1  22810  cpmadumatpoly  22827  cayleyhamilton  22834  1stcelcls  23405  imasdsf1olem  24317  comet  24457  nrmmetd  24518  tngngp  24598  tngngp3  24600  nmvs  24620  mulc1cncf  24854  cncfco  24856  pi1xfr  25011  pi1coghm  25017  caubl  25264  caublcls  25265  bcthlem2  25281  bcthlem3  25282  bcthlem4  25283  bcthlem5  25284  ivthlem2  25409  ovolicc2lem4  25477  volsuplem  25512  volsup  25513  uniioombllem3  25542  itg1climres  25671  itg2monolem1  25707  itg2i1fseqle  25711  itg2i1fseq  25712  itg2i1fseq2  25713  itg2addlem  25715  itgeq2  25735  dvferm1lem  25944  dvferm2lem  25946  dvlip  25954  c1lip1  25958  lhop1lem  25974  lhop1  25975  ftc1lem4  26002  ftc1lem6  26004  mdegmullem  26039  coe1mul3  26060  ply1divex  26098  coeeu  26186  coeeq  26188  coemullem  26211  coemul  26213  dvply1  26247  dvply2g  26248  dvply2gOLD  26249  aalioulem3  26298  aaliou3lem8  26309  ulmshftlem  26354  ulmshft  26355  ulmss  26362  pserdvlem2  26394  cxpcn3lem  26713  loglesqrt  26727  birthdaylem2  26918  emcllem2  26963  emcllem3  26964  harmonicbnd2  26971  lgamgulmlem2  26996  lgamgulmlem3  26997  lgamgulmlem5  26999  lgambdd  27003  lgamcvglem  27006  facgam  27032  ftalem7  27045  bposlem7  27257  bposlem9  27259  lgsqrlem2  27314  lgsqrlem4  27316  2lgslem3a  27363  2lgslem3b  27364  2lgslem3c  27365  2lgslem3d  27366  rplogsumlem1  27451  dchrvmasumlem1  27462  logsqvma  27509  logsqvma2  27510  selberglem3  27514  selberg  27515  selberg2lem  27517  selberg4lem1  27527  pntrsumo1  27532  selberg34r  27538  pntsval  27539  pntsval2  27543  pntrlog2bndlem1  27544  pntrlog2bndlem4  27547  pntpbnd  27555  pntibnd  27560  pntlemo  27574  addbday  28014  addonbday  28275  seqsval  28284  seqsp1  28307  bdaypw2n0bndlem  28459  ewlkinedg  29678  wkslem1  29681  uspgr2wlkeq  29719  wlkdlem2  29755  upgrwlkdvdelem  29809  crctcshwlkn0lem2  29884  crctcshwlkn0lem3  29885  crctcshwlkn0lem4  29886  crctcshwlkn0lem5  29887  wlkiswwlks2lem2  29943  wlkiswwlks2lem5  29946  wwlksnext  29966  wwlksnredwwlkn  29968  wwlksnextproplem2  29983  clwwlkccatlem  30064  clwlkclwwlklem2a1  30067  clwlkclwwlklem2fv1  30070  clwlkclwwlklem2a4  30072  clwlkclwwlklem2a  30073  clwlkclwwlklem2  30075  clwwisshclwwslemlem  30088  clwwisshclwws  30090  clwwlknlbonbgr1  30114  clwwlkel  30121  clwwlkf  30122  clwwlkwwlksb  30129  clwwlkext2edg  30131  wwlksext2clwwlk  30132  clwwlknonex2lem2  30183  eupthseg  30281  upgreupthseg  30284  eupth2lem3  30311  2clwwlk2clwwlklem  30421  2clwwlk  30422  numclwwlk1lem2f1  30432  numclwlk1lem2  30445  nvs  30738  nvtri  30745  ipval  30778  blocnilem  30879  phpar2  30898  phpar  30899  sii  30929  normsub0  31211  norm-ii  31213  norm-iii  31215  normsub  31218  normpyth  31220  norm3dif  31225  norm3lemt  31227  norm3adifi  31228  normpar  31230  polid  31234  bcs  31256  pjaddi  31761  pjsubi  31763  pjmuli  31764  pjcjt2  31767  lnopeq0lem2  32081  lnopunilem2  32086  branmfn  32180  hstel2  32294  stj  32310  cdj3lem1  32509  cdj3lem2b  32512  cdj3lem3b  32515  cdj3i  32516  ccatws1f1o  33033  gsummulsubdishift1  33151  elrgspnlem2  33325  constrsuc  33895  cnre2csqlem  34067  cnre2csqima  34068  mndpluscn  34083  lmdvg  34110  plymulx  34705  signsvfn  34739  subfacval2  35381  cvmliftlem7  35485  elmrsubrn  35714  faclim2  35942  fwddifval  36356  fwddifnval  36357  dnival  36671  unblimceq0lem  36706  unbdqndv2  36711  matunitlindf  37819  poimirlem32  37853  itg2gt0cn  37876  ftc1cnnclem  37892  ftc1cnnc  37893  areacirc  37914  sdclem1  37944  fdc  37946  seqpo  37948  incsequz  37949  incsequz2  37950  mettrifi  37958  caushft  37962  bfplem1  38023  ghomco  38092  rngohomadd  38170  rngohommul  38171  dihval  41502  lclkrlem1  41776  hdmap14lem2a  42137  hgmapval  42157  deg1pow  42405  sticksstones10  42419  sticksstones12a  42421  abvexp  42797  fsuppind  42843  prjspnval  42869  incssnn0  42963  rencldnfilem  43072  irrapxlem5  43078  irrapxlem6  43079  pellexlem3  43083  cvgdvgrat  44564  radcnvrat  44565  hashnzfzclim  44573  binomcxplemradcnv  44603  iunincfi  45348  monoords  45555  fperiodmullem  45561  monoordxrv  45735  monoordxr  45736  monoord2xrv  45737  monoord2xr  45738  climinf  45862  climsuse  45864  climinff  45867  mullimc  45872  mullimcf  45879  idlimc  45882  limcperiod  45884  limcrecl  45885  limclner  45905  climinf2  45961  climxrrelem  46003  cnrefiisplem  46083  cnrefiisp  46084  climxlim2lem  46099  cncfshift  46128  cncfperiod  46133  fperdvper  46173  dvnmul  46197  iblspltprt  46227  itgspltprt  46233  itgiccshift  46234  itgperiod  46235  dirkerval2  46348  dirkertrigeqlem1  46352  dirkertrigeqlem2  46353  dirkertrigeqlem3  46354  dirkercncflem2  46358  dirkercncflem3  46359  fourierdlem29  46390  elaa2lem  46487  elaa2  46488  nnfoctbdj  46710  meaiuninclem  46734  meaiunincf  46737  meaiuninc3v  46738  meaiuninc3  46739  meaiininclem  46740  meaiininc  46741  smflimlem6  47030  ormkglobd  47129  natglobalincr  47131  2ltceilhalf  47584  ceilhalfnn  47592  smonoord  47627  iccpartimp  47673  iccelpart  47689  icceuelpart  47692  fargshiftfv  47695  fmtnorec2  47799  bgoldbtbndlem2  48062  bgoldbtbndlem3  48063  bgoldbtbnd  48065  upgrimwlklem5  48157  gpgov  48298  gpg5nbgrvtx13starlem2  48328  ply1mulgsumlem3  48644  ply1mulgsumlem4  48645  ply1mulgsum  48646  ackvalsuc1  48935