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	|- ( A = B -> ( F ` ( A O C ) ) = ( F ` ( B O C ) ) )

Proof of Theorem fvoveq1

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( A = B -> A = B )
2	1	fvoveq1d 6110	1 |- ( A = B -> ( F ` ( A O C ) ) = ( F ` ( B O C ) ) )

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  10763  seq3val  10918  seqvalcd  10919  seqf  10922  seq3p1  10923  seqovcd  10925  seqp1cd  10928  seq3shft2  10939  seqshft2g  10940  seq3f1olemqsum  10971  seqhomog  10988  facp1  11190  lsw0  11374  ccatval1  11387  ccatval2  11388  ccatalpha  11403  swrdfv  11447  serf0  12143  fsumrelem  12263  mertenslemub  12326  mertenslemi1  12327  mertenslem2  12328  mertensabs  12329  bitsfval  12734  pcfac  13158  ennnfonelemj0  13350  ennnfonelemjn  13351  ennnfonelem0  13354  ennnfonelemp1  13355  ennnfonelemnn0  13371  nninfdclemcl  13397  nninfdclemp1  13399  nninfdc  13402  imasaddvallemg  13695  mhmlin  13833  mhmlem  13976  mulginvcom  14009  mhmmulg  14025  ghmlin  14110  psrmulvalfi  15188  comet  15725  mulc1cncf  15815  cncfco  15817  mulcncflem  15833  mulcncf  15834  ivthinclemlopn  15862  ivthinclemuopn  15864  limcimolemlt  15890  limccoap  15904  dvply1  15991  dvply2g  15992  eflt  16001  rpcxpef  16127  birthdaylem2  16226  pellexlem3  16231  bposlem7  16317  bposlem9  16319  2lgslem3a  16417  2lgslem3b  16418  2lgslem3c  16419  2lgslem3d  16420  wkslem1  16766  uspgr2wlkeq  16811  clwwlkccatlem  16846  clwwlkext2edg  16868  clwwlknonex2lem2  16884  eupthseg  16898  eupth2lem3fi  16922  depindlem1  16952  depindlem2  16953  depindlem3  16954