Theorem oveq1i 5542

Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)

Hypothesis

Ref	Expression
oveq1i.1	|- A = B

Assertion

Ref	Expression
oveq1i	|- ( A F C ) = ( B F C )

Proof of Theorem oveq1i

Step	Hyp	Ref	Expression
1		oveq1i.1	. 2 |- A = B
2		oveq1 5539	. 2 |- ( A = B -> ( A F C ) = ( B F C ) )
3	1, 2	ax-mp 7	1 |- ( A F C ) = ( B F C )

Syntax hints:   = wceq 1284  (class class class)co 5532

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-3an 921  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-rex 2354  df-v 2603  df-un 2977  df-sn 3404  df-pr 3405  df-op 3407  df-uni 3602  df-br 3786  df-iota 4887  df-fv 4930  df-ov 5535

This theorem is referenced by:  caov12  5709  halfnqq  6600  prarloclem5  6690  m1m1sr  6938  caucvgsrlemfv  6967  caucvgsr  6978  pitonnlem1  7013  axi2m1  7041  axcnre  7047  axcaucvg  7066  mvrraddi  7325  mvlladdi  7326  negsubdi  7364  mul02  7491  mulneg1  7499  mulreim  7704  recextlem1  7741  recdivap  7806  2p2e4  8159  2times  8160  3p2e5  8173  3p3e6  8174  4p2e6  8175  4p3e7  8176  4p4e8  8177  5p2e7  8178  5p3e8  8179  5p4e9  8180  6p2e8  8181  6p3e9  8182  7p2e9  8183  1mhlfehlf  8249  8th4div3  8250  halfpm6th  8251  nneoor  8449  9p1e10  8479  dfdec10  8480  num0h  8488  numsuc  8490  dec10p  8519  numma  8520  nummac  8521  numma2c  8522  numadd  8523  numaddc  8524  nummul2c  8526  decaddci  8537  decsubi  8539  decmul1  8540  5p5e10  8547  6p4e10  8548  7p3e10  8551  8p2e10  8556  decbin0  8616  decbin2  8617  elfzp1b  9114  elfzm1b  9115  qbtwnrelemcalc  9264  fldiv4p1lem1div2  9307  mulexpzap  9516  expaddzap  9520  cu2  9573  i3  9576  iexpcyc  9579  binom2i  9583  binom3  9590  3dec  9642  faclbnd  9668  bcm1k  9687  bcp1nk  9689  bcpasc  9693  imre  9738  crim  9745  remullem  9758  resqrexlemfp1  9895  resqrexlemover  9896  resqrexlemcalc1  9900  resqrexlemnm  9904  absexpzap  9966  absimle  9970  amgm2  10004  maxabslemlub  10093  3dvdsdec  10264  3dvds2dec  10265  odd2np1  10272  fz01or  10278  nn0o1gt2  10305  nn0o  10307  flodddiv4  10334  3lcm2e6woprm  10468  ex-fl  10563  ex-bc  10566  qdencn  10785