Theorem fvoveq1 6108

Description: Equality theorem for nested function and operation value. Closed form of fvoveq1d 6107. (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 6107	1 |- ( A = B -> ( F ` ( A O C ) ) = ( F ` ( B O C ) ) )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   ` cfv 5377  (class class class)co 6085

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 4131  df-iota 5337  df-fv 5385  df-ov 6088

This theorem is used by:  fldiv4lem1div2  10757  seq3val  10912  seqvalcd  10913  seqf  10916  seq3p1  10917  seqovcd  10919  seqp1cd  10922  seq3shft2  10933  seqshft2g  10934  seq3f1olemqsum  10965  seqhomog  10982  facp1  11184  lsw0  11368  ccatval1  11381  ccatval2  11382  ccatalpha  11397  swrdfv  11441  serf0  12137  fsumrelem  12257  mertenslemub  12320  mertenslemi1  12321  mertenslem2  12322  mertensabs  12323  bitsfval  12728  pcfac  13152  ennnfonelemj0  13344  ennnfonelemjn  13345  ennnfonelem0  13348  ennnfonelemp1  13349  ennnfonelemnn0  13365  nninfdclemcl  13391  nninfdclemp1  13393  nninfdc  13396  imasaddvallemg  13689  mhmlin  13827  mhmlem  13970  mulginvcom  14003  mhmmulg  14019  ghmlin  14104  psrmulvalfi  15160  comet  15691  mulc1cncf  15781  cncfco  15783  mulcncflem  15799  mulcncf  15800  ivthinclemlopn  15828  ivthinclemuopn  15830  limcimolemlt  15856  limccoap  15870  dvply1  15957  dvply2g  15958  eflt  15967  rpcxpef  16091  birthdaylem2  16187  pellexlem3  16192  bposlem7  16278  bposlem9  16280  2lgslem3a  16378  2lgslem3b  16379  2lgslem3c  16380  2lgslem3d  16381  wkslem1  16727  uspgr2wlkeq  16772  clwwlkccatlem  16807  clwwlkext2edg  16829  clwwlknonex2lem2  16845  eupthseg  16859  eupth2lem3fi  16883  depindlem1  16913  depindlem2  16914  depindlem3  16915