Theorem oveq1i 5824

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 5821	. 2 |- ( A = B -> ( A F C ) = ( B F C ) )
3	1, 2	ax-mp 5	1 |- ( A F C ) = ( B F C )

Syntax hints:   = wceq 1332  (class class class)co 5814

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-ext 2136

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1740  df-clab 2141  df-cleq 2147  df-clel 2150  df-nfc 2285  df-rex 2438  df-v 2711  df-un 3102  df-sn 3562  df-pr 3563  df-op 3565  df-uni 3769  df-br 3962  df-iota 5128  df-fv 5171  df-ov 5817

This theorem is referenced by:  caov12  5999  map1  6746  halfnqq  7309  prarloclem5  7399  m1m1sr  7660  caucvgsrlemfv  7690  caucvgsr  7701  pitonnlem1  7744  axi2m1  7774  axcnre  7780  axcaucvg  7799  mvrraddi  8071  mvlladdi  8072  negsubdi  8110  mul02  8241  mulneg1  8249  mulreim  8458  recextlem1  8504  recdivap  8570  2p2e4  8939  2times  8940  3p2e5  8953  3p3e6  8954  4p2e6  8955  4p3e7  8956  4p4e8  8957  5p2e7  8958  5p3e8  8959  5p4e9  8960  6p2e8  8961  6p3e9  8962  7p2e9  8963  1mhlfehlf  9030  8th4div3  9031  halfpm6th  9032  nneoor  9245  9p1e10  9276  dfdec10  9277  num0h  9285  numsuc  9287  dec10p  9316  numma  9317  nummac  9318  numma2c  9319  numadd  9320  numaddc  9321  nummul2c  9323  decaddci  9334  decsubi  9336  decmul1  9337  5p5e10  9344  6p4e10  9345  7p3e10  9348  8p2e10  9353  decbin0  9413  decbin2  9414  elfzp1b  9977  elfzm1b  9978  fz01or  9991  fz1ssfz0  9997  qbtwnrelemcalc  10133  fldiv4p1lem1div2  10182  1tonninf  10317  mulexpzap  10437  expaddzap  10441  sq4e2t8  10494  cu2  10495  i3  10498  iexpcyc  10501  binom2i  10505  binom3  10513  3dec  10565  faclbnd  10592  bcm1k  10611  bcp1nk  10613  bcpasc  10617  hashp1i  10661  hashxp  10677  imre  10728  crim  10735  remullem  10748  resqrexlemfp1  10886  resqrexlemover  10887  resqrexlemcalc1  10891  resqrexlemnm  10895  absexpzap  10957  absimle  10961  amgm2  10995  maxabslemlub  11084  fsumconst  11328  modfsummod  11332  binomlem  11357  binom11  11360  arisum  11372  arisum2  11373  georeclim  11387  geo2sum  11388  mertenslemi1  11409  mertenslem2  11410  mertensabs  11411  prodfrecap  11420  fprodm1s  11475  fprodp1s  11476  fprodrec  11503  fprodmodd  11515  efzval  11557  resinval  11589  recosval  11590  efi4p  11591  tan0  11605  efival  11606  cosadd  11611  cos2tsin  11625  ef01bndlem  11630  cos1bnd  11633  cos2bnd  11634  absefib  11644  efieq1re  11645  demoivreALT  11647  eirraplem  11650  3dvdsdec  11729  3dvds2dec  11730  odd2np1  11737  nn0o1gt2  11769  nn0o  11771  flodddiv4  11798  algrp1  11895  3lcm2e6woprm  11935  nn0gcdsq  12046  phiprmpw  12066  cnmpt1res  12643  rerestcntop  12897  dvfvalap  12997  dvcnp2cntop  13010  dveflem  13034  reeff1oleme  13040  sin0pilem1  13049  sinhalfpilem  13059  cospi  13068  eulerid  13070  cos2pi  13072  ef2kpi  13074  sinhalfpip  13088  sinhalfpim  13089  coshalfpip  13090  coshalfpim  13091  sincosq3sgn  13096  sincosq4sgn  13097  cosq23lt0  13101  tangtx  13106  sincos4thpi  13108  sincos6thpi  13110  cosq34lt1  13118  rplogb1  13212  2logb9irr  13235  sqrt2cxp2logb9e3  13239  2logb9irrap  13241  ex-fl  13247  ex-exp  13249  ex-bc  13251  012of  13514  2o01f  13515  qdencn  13547  isomninnlem  13550  iswomninnlem  13569  ismkvnnlem  13572