Theorem fvoveq1 7390

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

Syntax hints:   → wi 4   = wceq 1542  ‘cfv 6498  (class class class)co 7367

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370

This theorem is referenced by:  coof  7655  fldiv4p1lem1div2  13794  fldiv4lem1div2  13796  modval  13830  seqval  13974  seqp1  13978  seqshft2  13990  monoord  13994  monoord2  13995  seqhomo  14011  facp1  14240  faclbnd4lem2  14256  bcval  14266  lsw0  14527  ccatval1  14539  ccatval2  14540  ccatalpha  14556  swrdfv  14611  2swrd2eqwrdeq  14915  imval  15069  recan  15299  rlimcld2  15540  rlimcn1  15550  rlimcn3  15552  climcn1  15554  climcn2  15555  subcn2  15557  o1of2  15575  isercoll2  15631  climsup  15632  serf0  15643  iseraltlem2  15645  fsumrelem  15770  mertenslem1  15849  mertenslem2  15850  mertens  15851  bitsfval  16392  smuval  16450  pcfac  16870  vdwlem6  16957  vdwlem8  16959  vdwlem9  16960  vdwlem10  16961  imasaddvallem  17493  imasvscafn  17501  imasvscaval  17502  chnltm1  18575  chnind  18587  mgmhmlin  18667  mhmlin  18761  mhmlem  19038  mulginvcom  19075  mhmmulg  19091  ghmlin  19196  efgsdm  19705  efgsdmi  19707  efgsrel  19709  efgsp1  19712  frgpup1  19750  rnghmmul  20429  c0snmgmhm  20442  zrrnghm  20513  abvmul  20798  abvtri  20799  issrngd  20832  lmhmlin  21030  ipcj  21614  psrmulval  21923  mhpmulcl  22115  psdcoef  22126  psdadd  22129  psdpw  22136  coe1mul2  22234  coe1tmmul2fv  22243  coe1pwmulfv  22245  cply1mul  22261  mat1scmat  22504  mdetmul  22588  madufval  22602  cramer0  22655  cpmatmcllem  22683  d1mat2pmat  22704  m2cpminvid2lem  22719  decpmatmullem  22736  decpmatmulsumfsupp  22738  pm2mpmhmlem1  22783  pm2mpmhmlem2  22784  cayhamlem1  22831  cpmadumatpoly  22848  cayleyhamilton  22855  1stcelcls  23426  imasdsf1olem  24338  comet  24478  nrmmetd  24539  tngngp  24619  tngngp3  24621  nmvs  24641  mulc1cncf  24872  cncfco  24874  pi1xfr  25022  pi1coghm  25028  caubl  25275  caublcls  25276  bcthlem2  25292  bcthlem3  25293  bcthlem4  25294  bcthlem5  25295  ivthlem2  25419  ovolicc2lem4  25487  volsuplem  25522  volsup  25523  uniioombllem3  25552  itg1climres  25681  itg2monolem1  25717  itg2i1fseqle  25721  itg2i1fseq  25722  itg2i1fseq2  25723  itg2addlem  25725  itgeq2  25745  dvferm1lem  25951  dvferm2lem  25953  dvlip  25960  c1lip1  25964  lhop1lem  25980  lhop1  25981  ftc1lem4  26006  ftc1lem6  26008  mdegmullem  26043  coe1mul3  26064  ply1divex  26102  coeeu  26190  coeeq  26192  coemullem  26215  coemul  26217  dvply1  26250  dvply2g  26251  aalioulem3  26300  aaliou3lem8  26311  ulmshftlem  26354  ulmshft  26355  ulmss  26362  pserdvlem2  26393  cxpcn3lem  26711  loglesqrt  26725  birthdaylem2  26916  emcllem2  26960  emcllem3  26961  harmonicbnd2  26968  lgamgulmlem2  26993  lgamgulmlem3  26994  lgamgulmlem5  26996  lgambdd  27000  lgamcvglem  27003  facgam  27029  ftalem7  27042  bposlem7  27253  bposlem9  27255  lgsqrlem2  27310  lgsqrlem4  27312  2lgslem3a  27359  2lgslem3b  27360  2lgslem3c  27361  2lgslem3d  27362  rplogsumlem1  27447  dchrvmasumlem1  27458  logsqvma  27505  logsqvma2  27506  selberglem3  27510  selberg  27511  selberg2lem  27513  selberg4lem1  27523  pntrsumo1  27528  selberg34r  27534  pntsval  27535  pntsval2  27539  pntrlog2bndlem1  27540  pntrlog2bndlem4  27543  pntpbnd  27551  pntibnd  27556  pntlemo  27570  addbday  28010  addonbday  28271  seqsval  28280  seqsp1  28303  bdaypw2n0bndlem  28455  ewlkinedg  29673  wkslem1  29676  uspgr2wlkeq  29714  wlkdlem2  29750  upgrwlkdvdelem  29804  crctcshwlkn0lem2  29879  crctcshwlkn0lem3  29880  crctcshwlkn0lem4  29881  crctcshwlkn0lem5  29882  wlkiswwlks2lem2  29938  wlkiswwlks2lem5  29941  wwlksnext  29961  wwlksnredwwlkn  29963  wwlksnextproplem2  29978  clwwlkccatlem  30059  clwlkclwwlklem2a1  30062  clwlkclwwlklem2fv1  30065  clwlkclwwlklem2a4  30067  clwlkclwwlklem2a  30068  clwlkclwwlklem2  30070  clwwisshclwwslemlem  30083  clwwisshclwws  30085  clwwlknlbonbgr1  30109  clwwlkel  30116  clwwlkf  30117  clwwlkwwlksb  30124  clwwlkext2edg  30126  wwlksext2clwwlk  30127  clwwlknonex2lem2  30178  eupthseg  30276  upgreupthseg  30279  eupth2lem3  30306  2clwwlk2clwwlklem  30416  2clwwlk  30417  numclwwlk1lem2f1  30427  numclwlk1lem2  30440  nvs  30734  nvtri  30741  ipval  30774  blocnilem  30875  phpar2  30894  phpar  30895  sii  30925  normsub0  31207  norm-ii  31209  norm-iii  31211  normsub  31214  normpyth  31216  norm3dif  31221  norm3lemt  31223  norm3adifi  31224  normpar  31226  polid  31230  bcs  31252  pjaddi  31757  pjsubi  31759  pjmuli  31760  pjcjt2  31763  lnopeq0lem2  32077  lnopunilem2  32082  branmfn  32176  hstel2  32290  stj  32306  cdj3lem1  32505  cdj3lem2b  32508  cdj3lem3b  32511  cdj3i  32512  ccatws1f1o  33011  gsummulsubdishift1  33129  elrgspnlem2  33304  constrsuc  33882  cnre2csqlem  34054  cnre2csqima  34055  mndpluscn  34070  lmdvg  34097  plymulx  34692  signsvfn  34726  subfacval2  35369  cvmliftlem7  35473  elmrsubrn  35702  faclim2  35930  fwddifval  36344  fwddifnval  36345  dnival  36731  unblimceq0lem  36766  unbdqndv2  36771  matunitlindf  37939  poimirlem32  37973  itg2gt0cn  37996  ftc1cnnclem  38012  ftc1cnnc  38013  areacirc  38034  sdclem1  38064  fdc  38066  seqpo  38068  incsequz  38069  incsequz2  38070  mettrifi  38078  caushft  38082  bfplem1  38143  ghomco  38212  rngohomadd  38290  rngohommul  38291  dihval  41678  lclkrlem1  41952  hdmap14lem2a  42313  hgmapval  42333  deg1pow  42580  sticksstones10  42594  sticksstones12a  42596  abvexp  42977  fsuppind  43023  prjspnval  43049  incssnn0  43143  rencldnfilem  43248  irrapxlem5  43254  irrapxlem6  43255  pellexlem3  43259  cvgdvgrat  44740  radcnvrat  44741  hashnzfzclim  44749  binomcxplemradcnv  44779  iunincfi  45524  monoords  45730  fperiodmullem  45736  monoordxrv  45909  monoordxr  45910  monoord2xrv  45911  monoord2xr  45912  climinf  46036  climsuse  46038  climinff  46041  mullimc  46046  mullimcf  46053  idlimc  46056  limcperiod  46058  limcrecl  46059  limclner  46079  climinf2  46135  climxrrelem  46177  cnrefiisplem  46257  cnrefiisp  46258  climxlim2lem  46273  cncfshift  46302  cncfperiod  46307  fperdvper  46347  dvnmul  46371  iblspltprt  46401  itgspltprt  46407  itgiccshift  46408  itgperiod  46409  dirkerval2  46522  dirkertrigeqlem1  46526  dirkertrigeqlem2  46527  dirkertrigeqlem3  46528  dirkercncflem2  46532  dirkercncflem3  46533  fourierdlem29  46564  elaa2lem  46661  elaa2  46662  nnfoctbdj  46884  meaiuninclem  46908  meaiunincf  46911  meaiuninc3v  46912  meaiuninc3  46913  meaiininclem  46914  meaiininc  46915  smflimlem6  47204  ormkglobd  47305  natglobalincr  47307  2ltceilhalf  47780  ceilhalfnn  47788  smonoord  47825  iccpartimp  47877  iccelpart  47893  icceuelpart  47896  fargshiftfv  47899  fmtnorec2  48006  ppivalnnnprmge6  48089  ppivalnnnprm  48091  ppivalnn  48095  bgoldbtbndlem2  48282  bgoldbtbndlem3  48283  bgoldbtbnd  48285  upgrimwlklem5  48377  gpgov  48518  gpg5nbgrvtx13starlem2  48548  ply1mulgsumlem3  48864  ply1mulgsumlem4  48865  ply1mulgsum  48866  ackvalsuc1  49155