Theorem fvoveq1 6081

Description: Equality theorem for nested function and operation value. Closed form of fvoveq1d 6080. (Contributed by AV, 23-Jul-2022.)

Assertion

Ref	Expression
fvoveq1	⊢ (𝐴 = 𝐵 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶)))

Proof of Theorem fvoveq1

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	fvoveq1d 6080	1 ⊢ (𝐴 = 𝐵 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶)))

Syntax hints:   → wi 4   = wceq 1398  ‘cfv 5357  (class class class)co 6058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-v 2817  df-un 3218  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-iota 5317  df-fv 5365  df-ov 6061

This theorem is referenced by:  fldiv4lem1div2  10691  seq3val  10846  seqvalcd  10847  seqf  10850  seq3p1  10851  seqovcd  10853  seqp1cd  10856  seq3shft2  10867  seqshft2g  10868  seq3f1olemqsum  10899  seqhomog  10916  facp1  11117  lsw0  11297  ccatval1  11310  ccatval2  11311  ccatalpha  11326  swrdfv  11370  serf0  12062  fsumrelem  12182  mertenslemub  12245  mertenslemi1  12246  mertenslem2  12247  mertensabs  12248  bitsfval  12653  pcfac  13073  ennnfonelemj0  13236  ennnfonelemjn  13237  ennnfonelem0  13240  ennnfonelemp1  13241  ennnfonelemnn0  13257  nninfdclemcl  13283  nninfdclemp1  13285  nninfdc  13288  imasaddvallemg  13579  mhmlin  13722  mhmlem  13867  mulginvcom  13900  mhmmulg  13916  ghmlin  14001  comet  15490  mulc1cncf  15580  cncfco  15582  mulcncflem  15598  mulcncf  15599  ivthinclemlopn  15627  ivthinclemuopn  15629  limcimolemlt  15655  limccoap  15669  dvply1  15756  dvply2g  15757  eflt  15766  rpcxpef  15885  pellexlem3  15973  2lgslem3a  16092  2lgslem3b  16093  2lgslem3c  16094  2lgslem3d  16095  wkslem1  16441  uspgr2wlkeq  16486  clwwlkccatlem  16521  clwwlkext2edg  16543  clwwlknonex2lem2  16559  eupthseg  16573  eupth2lem3fi  16597  depindlem1  16627  depindlem2  16628  depindlem3  16629