Theorem fvoveq1 6041

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

Syntax hints:   → wi 4   = wceq 1397  ‘cfv 5326  (class class class)co 6018

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6021

This theorem is referenced by:  fldiv4lem1div2  10568  seq3val  10723  seqvalcd  10724  seqf  10727  seq3p1  10728  seqovcd  10730  seqp1cd  10733  seq3shft2  10744  seqshft2g  10745  seq3f1olemqsum  10776  seqhomog  10793  facp1  10993  lsw0  11165  ccatval1  11178  ccatval2  11179  ccatalpha  11194  swrdfv  11238  serf0  11930  fsumrelem  12050  mertenslemub  12113  mertenslemi1  12114  mertenslem2  12115  mertensabs  12116  bitsfval  12521  pcfac  12941  ennnfonelemj0  13040  ennnfonelemjn  13041  ennnfonelem0  13044  ennnfonelemp1  13045  ennnfonelemnn0  13061  nninfdclemcl  13087  nninfdclemp1  13089  nninfdc  13092  imasaddvallemg  13416  mhmlin  13568  mhmlem  13719  mulginvcom  13752  mhmmulg  13768  ghmlin  13853  comet  15242  mulc1cncf  15332  cncfco  15334  mulcncflem  15350  mulcncf  15351  ivthinclemlopn  15379  ivthinclemuopn  15381  limcimolemlt  15407  limccoap  15421  dvply1  15508  dvply2g  15509  eflt  15518  rpcxpef  15637  2lgslem3a  15841  2lgslem3b  15842  2lgslem3c  15843  2lgslem3d  15844  wkslem1  16190  uspgr2wlkeq  16235  clwwlkccatlem  16270  clwwlkext2edg  16292  clwwlknonex2lem2  16308  eupthseg  16322  eupth2lem3fi  16346  depindlem1  16376  depindlem2  16377  depindlem3  16378