Theorem fvoveq1 6051

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

Syntax hints:   → wi 4   = wceq 1398  ‘cfv 5333  (class class class)co 6028

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 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rex 2517  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-iota 5293  df-fv 5341  df-ov 6031

This theorem is referenced by:  fldiv4lem1div2  10613  seq3val  10768  seqvalcd  10769  seqf  10772  seq3p1  10773  seqovcd  10775  seqp1cd  10778  seq3shft2  10789  seqshft2g  10790  seq3f1olemqsum  10821  seqhomog  10838  facp1  11038  lsw0  11210  ccatval1  11223  ccatval2  11224  ccatalpha  11239  swrdfv  11283  serf0  11975  fsumrelem  12095  mertenslemub  12158  mertenslemi1  12159  mertenslem2  12160  mertensabs  12161  bitsfval  12566  pcfac  12986  ennnfonelemj0  13085  ennnfonelemjn  13086  ennnfonelem0  13089  ennnfonelemp1  13090  ennnfonelemnn0  13106  nninfdclemcl  13132  nninfdclemp1  13134  nninfdc  13137  imasaddvallemg  13461  mhmlin  13613  mhmlem  13764  mulginvcom  13797  mhmmulg  13813  ghmlin  13898  comet  15293  mulc1cncf  15383  cncfco  15385  mulcncflem  15401  mulcncf  15402  ivthinclemlopn  15430  ivthinclemuopn  15432  limcimolemlt  15458  limccoap  15472  dvply1  15559  dvply2g  15560  eflt  15569  rpcxpef  15688  pellexlem3  15776  2lgslem3a  15895  2lgslem3b  15896  2lgslem3c  15897  2lgslem3d  15898  wkslem1  16244  uspgr2wlkeq  16289  clwwlkccatlem  16324  clwwlkext2edg  16346  clwwlknonex2lem2  16362  eupthseg  16376  eupth2lem3fi  16400  depindlem1  16430  depindlem2  16431  depindlem3  16432