Theorem oveq1i 5676

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 5673	. 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 1290  (class class class)co 5666

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071

This theorem depends on definitions:  df-bi 116  df-3an 927  df-tru 1293  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-rex 2366  df-v 2622  df-un 3004  df-sn 3456  df-pr 3457  df-op 3459  df-uni 3660  df-br 3852  df-iota 4993  df-fv 5036  df-ov 5669

This theorem is referenced by:  caov12  5847  map1  6583  halfnqq  7023  prarloclem5  7113  m1m1sr  7361  caucvgsrlemfv  7390  caucvgsr  7401  pitonnlem1  7436  axi2m1  7464  axcnre  7470  axcaucvg  7489  mvrraddi  7753  mvlladdi  7754  negsubdi  7792  mul02  7919  mulneg1  7927  mulreim  8135  recextlem1  8174  recdivap  8239  2p2e4  8597  2times  8598  3p2e5  8611  3p3e6  8612  4p2e6  8613  4p3e7  8614  4p4e8  8615  5p2e7  8616  5p3e8  8617  5p4e9  8618  6p2e8  8619  6p3e9  8620  7p2e9  8621  1mhlfehlf  8688  8th4div3  8689  halfpm6th  8690  nneoor  8902  9p1e10  8933  dfdec10  8934  num0h  8942  numsuc  8944  dec10p  8973  numma  8974  nummac  8975  numma2c  8976  numadd  8977  numaddc  8978  nummul2c  8980  decaddci  8991  decsubi  8993  decmul1  8994  5p5e10  9001  6p4e10  9002  7p3e10  9005  8p2e10  9010  decbin0  9070  decbin2  9071  elfzp1b  9565  elfzm1b  9566  fz01or  9579  fz1ssfz0  9585  qbtwnrelemcalc  9721  fldiv4p1lem1div2  9766  1tonninf  9900  mulexpzap  10049  expaddzap  10053  sq4e2t8  10106  cu2  10107  i3  10110  iexpcyc  10113  binom2i  10117  binom3  10125  3dec  10177  faclbnd  10203  bcm1k  10222  bcp1nk  10224  bcpasc  10228  hashp1i  10272  hashxp  10288  imre  10339  crim  10346  remullem  10359  resqrexlemfp1  10496  resqrexlemover  10497  resqrexlemcalc1  10501  resqrexlemnm  10505  absexpzap  10567  absimle  10571  amgm2  10605  maxabslemlub  10694  fsumconst  10902  modfsummod  10906  binomlem  10931  binom11  10934  arisum  10946  arisum2  10947  georeclim  10961  geo2sum  10962  mertenslemi1  10983  mertenslem2  10984  mertensabs  10985  efzval  11027  resinval  11060  recosval  11061  efi4p  11062  tan0  11076  efival  11077  cosadd  11082  cos2tsin  11096  ef01bndlem  11101  cos1bnd  11104  cos2bnd  11105  absefib  11114  efieq1re  11115  demoivreALT  11117  eirraplem  11118  3dvdsdec  11197  3dvds2dec  11198  odd2np1  11205  nn0o1gt2  11237  nn0o  11239  flodddiv4  11266  algrp1  11360  3lcm2e6woprm  11400  nn0gcdsq  11510  phiprmpw  11530  ex-fl  11918  ex-exp  11920  ex-bc  11922  qdencn  12181