Theorem fvoveq1 6111

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402  ‘cfv 5380  (class class class)co 6088

This proof depends on 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 proof 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 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4132  df-iota 5340  df-fv 5388  df-ov 6091

This theorem is used by:  fldiv4lem1div2  10762  seq3val  10917  seqvalcd  10918  seqf  10921  seq3p1  10922  seqovcd  10924  seqp1cd  10927  seq3shft2  10938  seqshft2g  10939  seq3f1olemqsum  10970  seqhomog  10987  facp1  11189  lsw0  11373  ccatval1  11386  ccatval2  11387  ccatalpha  11402  swrdfv  11446  serf0  12142  fsumrelem  12262  mertenslemub  12325  mertenslemi1  12326  mertenslem2  12327  mertensabs  12328  bitsfval  12733  pcfac  13157  ennnfonelemj0  13349  ennnfonelemjn  13350  ennnfonelem0  13353  ennnfonelemp1  13354  ennnfonelemnn0  13370  nninfdclemcl  13396  nninfdclemp1  13398  nninfdc  13401  imasaddvallemg  13694  mhmlin  13832  mhmlem  13975  mulginvcom  14008  mhmmulg  14024  ghmlin  14109  psrmulvalfi  15197  comet  15742  mulc1cncf  15832  cncfco  15834  mulcncflem  15850  mulcncf  15851  ivthinclemlopn  15879  ivthinclemuopn  15881  limcimolemlt  15907  limccoap  15921  dvply1  16008  dvply2g  16009  eflt  16018  rpcxpef  16144  birthdaylem2  16243  pellexlem3  16248  bposlem7  16334  bposlem9  16336  2lgslem3a  16434  2lgslem3b  16435  2lgslem3c  16436  2lgslem3d  16437  wkslem1  16783  uspgr2wlkeq  16828  clwwlkccatlem  16863  clwwlkext2edg  16885  clwwlknonex2lem2  16901  eupthseg  16915  eupth2lem3fi  16939  depindlem1  16969  depindlem2  16970  depindlem3  16971