Theorem fvoveq1 5898

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

Syntax hints:   -> wi 4   = wceq 1353   ` cfv 5217  (class class class)co 5875

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2740  df-un 3134  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-br 4005  df-iota 5179  df-fv 5225  df-ov 5878

This theorem is referenced by:  seq3val  10458  seqvalcd  10459  seqf  10461  seq3p1  10462  seqovcd  10463  seqp1cd  10466  seq3shft2  10473  seq3f1olemqsum  10500  facp1  10710  serf0  11360  fsumrelem  11479  mertenslemub  11542  mertenslemi1  11543  mertenslem2  11544  mertensabs  11545  pcfac  12348  ennnfonelemj0  12402  ennnfonelemjn  12403  ennnfonelem0  12406  ennnfonelemp1  12407  ennnfonelemnn0  12423  nninfdclemcl  12449  nninfdclemp1  12451  nninfdc  12454  imasaddvallemg  12736  mhmlin  12858  mhmlem  12978  mulginvcom  13008  mhmmulg  13024  comet  14002  mulc1cncf  14079  cncfco  14081  mulcncflem  14093  mulcncf  14094  ivthinclemlopn  14117  ivthinclemuopn  14119  limcimolemlt  14136  limccoap  14150  eflt  14199  rpcxpef  14318