Theorem fvoveq1 6101

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

Syntax hints:   → wi 4   = wceq 1402  ‘cfv 5375  (class class class)co 6078

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823  df-un 3224  df-sn 3714  df-pr 3715  df-op 3717  df-uni 3934  df-br 4129  df-iota 5335  df-fv 5383  df-ov 6081

This theorem is referenced by:  fldiv4lem1div2  10723  seq3val  10878  seqvalcd  10879  seqf  10882  seq3p1  10883  seqovcd  10885  seqp1cd  10888  seq3shft2  10899  seqshft2g  10900  seq3f1olemqsum  10931  seqhomog  10948  facp1  11149  lsw0  11333  ccatval1  11346  ccatval2  11347  ccatalpha  11362  swrdfv  11406  serf0  12099  fsumrelem  12219  mertenslemub  12282  mertenslemi1  12283  mertenslem2  12284  mertensabs  12285  bitsfval  12690  pcfac  13110  ennnfonelemj0  13273  ennnfonelemjn  13274  ennnfonelem0  13277  ennnfonelemp1  13278  ennnfonelemnn0  13294  nninfdclemcl  13320  nninfdclemp1  13322  nninfdc  13325  imasaddvallemg  13616  mhmlin  13754  mhmlem  13897  mulginvcom  13930  mhmmulg  13946  ghmlin  14031  comet  15526  mulc1cncf  15616  cncfco  15618  mulcncflem  15634  mulcncf  15635  ivthinclemlopn  15663  ivthinclemuopn  15665  limcimolemlt  15691  limccoap  15705  dvply1  15792  dvply2g  15793  eflt  15802  rpcxpef  15922  pellexlem3  16010  2lgslem3a  16129  2lgslem3b  16130  2lgslem3c  16131  2lgslem3d  16132  wkslem1  16478  uspgr2wlkeq  16523  clwwlkccatlem  16558  clwwlkext2edg  16580  clwwlknonex2lem2  16596  eupthseg  16610  eupth2lem3fi  16634  depindlem1  16664  depindlem2  16665  depindlem3  16666