Theorem fvoveq1 5969

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

Syntax hints:   -> wi 4   = wceq 1373   ` cfv 5272  (class class class)co 5946

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4046  df-iota 5233  df-fv 5280  df-ov 5949

This theorem is referenced by:  fldiv4lem1div2  10452  seq3val  10607  seqvalcd  10608  seqf  10611  seq3p1  10612  seqovcd  10614  seqp1cd  10617  seq3shft2  10628  seqshft2g  10629  seq3f1olemqsum  10660  seqhomog  10677  facp1  10877  lsw0  11043  ccatval1  11056  ccatval2  11057  swrdfv  11109  serf0  11696  fsumrelem  11815  mertenslemub  11878  mertenslemi1  11879  mertenslem2  11880  mertensabs  11881  bitsfval  12286  pcfac  12706  ennnfonelemj0  12805  ennnfonelemjn  12806  ennnfonelem0  12809  ennnfonelemp1  12810  ennnfonelemnn0  12826  nninfdclemcl  12852  nninfdclemp1  12854  nninfdc  12857  imasaddvallemg  13180  mhmlin  13332  mhmlem  13483  mulginvcom  13516  mhmmulg  13532  ghmlin  13617  comet  15004  mulc1cncf  15094  cncfco  15096  mulcncflem  15112  mulcncf  15113  ivthinclemlopn  15141  ivthinclemuopn  15143  limcimolemlt  15169  limccoap  15183  dvply1  15270  dvply2g  15271  eflt  15280  rpcxpef  15399  2lgslem3a  15603  2lgslem3b  15604  2lgslem3c  15605  2lgslem3d  15606