Theorem oveq1i 6028

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 6025	. 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 1397  (class class class)co 6018

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6021

This theorem is referenced by:  caov12  6211  map1  6987  exmidpw2en  7104  halfnqq  7630  prarloclem5  7720  m1m1sr  7981  caucvgsrlemfv  8011  caucvgsr  8022  pitonnlem1  8065  axi2m1  8095  axcnre  8101  axcaucvg  8120  mvrraddi  8396  mvlladdi  8397  negsubdi  8435  mul02  8566  mulneg1  8574  mulreim  8784  recextlem1  8831  recdivap  8898  2p2e4  9270  2times  9271  3p2e5  9285  3p3e6  9286  4p2e6  9287  4p3e7  9288  4p4e8  9289  5p2e7  9290  5p3e8  9291  5p4e9  9292  6p2e8  9293  6p3e9  9294  7p2e9  9295  1mhlfehlf  9362  8th4div3  9363  halfpm6th  9364  nneoor  9582  9p1e10  9613  dfdec10  9614  num0h  9622  numsuc  9624  dec10p  9653  numma  9654  nummac  9655  numma2c  9656  numadd  9657  numaddc  9658  nummul2c  9660  decaddci  9671  decsubi  9673  decmul1  9674  5p5e10  9681  6p4e10  9682  7p3e10  9685  8p2e10  9690  decbin0  9750  decbin2  9751  elfzp1b  10332  elfzm1b  10333  fz01or  10346  fz1ssfz0  10352  fz0to4untppr  10359  qbtwnrelemcalc  10516  fldiv4p1lem1div2  10566  1tonninf  10704  mulexpzap  10842  expaddzap  10846  sq4e2t8  10900  cu2  10901  i3  10904  iexpcyc  10907  binom2i  10911  binom3  10920  3dec  10977  faclbnd  11004  bcm1k  11023  bcp1nk  11025  bcpasc  11029  hashp1i  11075  hashxp  11091  ccatlid  11187  pfxccatin12lem2c  11315  imre  11429  crim  11436  remullem  11449  resqrexlemfp1  11587  resqrexlemover  11588  resqrexlemcalc1  11592  resqrexlemnm  11596  absexpzap  11658  absimle  11662  amgm2  11696  maxabslemlub  11785  fsumconst  12033  modfsummod  12037  binomlem  12062  binom11  12065  arisum  12077  arisum2  12078  georeclim  12092  geo2sum  12093  mertenslemi1  12114  mertenslem2  12115  mertensabs  12116  prodfrecap  12125  fprodm1s  12180  fprodp1s  12181  fprodrec  12208  fprodmodd  12220  efzval  12262  resinval  12294  recosval  12295  efi4p  12296  tan0  12310  efival  12311  cosadd  12316  cos2tsin  12330  ef01bndlem  12335  cos1bnd  12338  cos2bnd  12339  absefib  12350  efieq1re  12351  demoivreALT  12353  eirraplem  12356  3dvds  12443  3dvdsdec  12444  3dvds2dec  12445  odd2np1  12452  nn0o1gt2  12484  nn0o  12486  5ndvds3  12513  5ndvds6  12514  flodddiv4  12515  m1bits  12539  algrp1  12636  3lcm2e6woprm  12676  nn0gcdsq  12790  phiprmpw  12812  prmdiv  12825  prmdiveq  12826  pythagtriplem1  12856  pythagtriplem12  12866  pythagtriplem14  12868  pockthi  12949  infpnlem1  12950  4sqlem12  12993  4sqlem13m  12994  4sqlem19  13000  dec5dvds  13003  dec5nprm  13005  dec2nprm  13006  modxai  13007  modxp1i  13009  modsubi  13010  gcdmodi  13012  decsplit0b  13017  decsplit1  13019  decsplit  13020  karatsuba  13021  2exp7  13025  2exp8  13026  3exp3  13029  pwsbas  13393  subsubm  13584  mulg2  13736  subsubg  13802  unitsubm  14152  subsubrng  14247  subsubrg  14278  lsslss  14414  expghmap  14640  cnmpt1res  15039  rerestcntop  15301  rerest  15303  dvfvalap  15424  dvcnp2cntop  15442  dveflem  15469  plyun0  15479  dvply1  15508  reeff1oleme  15515  sin0pilem1  15524  sinhalfpilem  15534  cospi  15543  eulerid  15545  cos2pi  15547  ef2kpi  15549  sinhalfpip  15563  sinhalfpim  15564  coshalfpip  15565  coshalfpim  15566  sincosq3sgn  15571  sincosq4sgn  15572  cosq23lt0  15576  tangtx  15581  sincos4thpi  15583  sincos6thpi  15585  cosq34lt1  15593  rplogb1  15691  2logb9irr  15714  sqrt2cxp2logb9e3  15718  2logb9irrap  15720  binom4  15722  lgsdir2lem1  15776  lgsdir2lem2  15777  lgsdir2lem4  15779  lgsdir2lem5  15780  lgsne0  15786  1lgs  15791  gausslemma2dlem0e  15801  gausslemma2dlem0f  15802  gausslemma2dlem3  15811  gausslemma2d  15817  lgseisenlem1  15818  lgseisenlem2  15819  lgseisenlem3  15820  lgseisenlem4  15821  lgseisen  15822  lgsquadlem1  15825  lgsquadlem2  15826  lgsquad2lem1  15829  lgsquad2lem2  15830  m1lgs  15833  2lgslem3a  15841  2lgslem3b  15842  2lgslem3c  15843  2lgslem3d  15844  2lgsoddprmlem3a  15855  2lgsoddprmlem3b  15856  2lgsoddprmlem3c  15857  2lgsoddprmlem3d  15858  ex-fl  16368  ex-exp  16370  ex-bc  16372  depindlem1  16376  012of  16643  2o01f  16644  qdencn  16682  isomninnlem  16685  iswomninnlem  16705  ismkvnnlem  16708