Theorem oveq1i 6098

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

This proof depends on syntax axioms:   = wceq 1402  (class class class)co 6088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4132  df-iota 5340  df-fv 5388  df-ov 6091

This theorem is used by:  caov12  6281  map1  7107  exmidpw2en  7225  halfnqq  7783  prarloclem5  7873  m1m1sr  8134  caucvgsrlemfv  8164  caucvgsr  8175  pitonnlem1  8218  axi2m1  8248  axcnre  8254  axcaucvg  8273  mvrraddi  8550  mvlladdi  8551  negsubdi  8589  mul02  8721  mulneg1  8729  mulreim  8940  recextlem1  8987  recdivap  9056  2p2e4  9440  2times  9441  3p2e5  9455  3p3e6  9456  4p2e6  9457  4p3e7  9458  4p4e8  9459  5p2e7  9460  5p3e8  9461  5p4e9  9462  6p2e8  9463  6p3e9  9464  7p2e9  9465  1mhlfehlf  9534  8th4div3  9535  halfpm6th  9536  nneoor  9758  9p1e10  9789  dfdec10  9790  num0h  9798  numsuc  9800  dec10p  9834  numma  9835  nummac  9836  numma2c  9837  numadd  9838  numaddc  9839  nummul2c  9841  decaddci  9852  decsubi  9854  decmul1  9855  5p5e10  9862  6p4e10  9863  7p3e10  9866  8p2e10  9871  decbin0  9931  decbin2  9932  elfzp1b  10520  elfzm1b  10521  fz01or  10534  fz1ssfz0  10540  fz0to4untppr  10547  qbtwnrelemcalc  10706  fldiv4p1lem1div2  10760  1tonninf  10898  mulexpzap  11036  expaddzap  11040  sq4e2t8  11094  cu2  11095  i3  11098  iexpcyc  11101  binom2i  11105  binom3  11114  3dec  11173  faclbnd  11200  bcm1k  11219  bcp1nk  11221  bcpasc  11225  hashp1i  11272  hashxp  11288  hashpwfi  11290  hashfibc  11304  ccatlid  11395  pfxccatin12lem2c  11523  imre  11637  crim  11644  remullem  11657  sq01  11681  resqrexlemfp1  11796  resqrexlemover  11797  resqrexlemcalc1  11801  resqrexlemnm  11805  absexpzap  11868  absimle  11872  amgm2  11906  maxabslemlub  11995  fsumconst  12245  modfsummod  12249  binomlem  12274  binom11  12277  arisum  12289  arisum2  12290  georeclim  12304  geo2sum  12305  mertenslemi1  12326  mertenslem2  12327  mertensabs  12328  prodfrecap  12337  fprodm1s  12392  fprodp1s  12393  fprodrec  12420  fprodmodd  12432  efzval  12474  resinval  12506  recosval  12507  efi4p  12508  tan0  12522  efival  12523  cosadd  12528  cos2tsin  12542  ef01bndlem  12547  cos1bnd  12550  cos2bnd  12551  absefib  12562  efieq1re  12563  demoivreALT  12565  eirraplem  12568  3dvds  12655  3dvdsdec  12656  3dvds2dec  12657  odd2np1  12664  nn0o1gt2  12696  nn0o  12698  5ndvds3  12725  5ndvds6  12726  flodddiv4  12727  m1bits  12751  algrp1  12848  3lcm2e6woprm  12888  nn0gcdsq  13004  phiprmpw  13028  prmdiv  13041  prmdiveq  13042  pythagtriplem1  13072  pythagtriplem12  13082  pythagtriplem14  13084  pockthi  13165  infpnlem1  13166  4sqlem12  13209  4sqlem13m  13210  4sqlem19  13216  dec5dvds  13219  dec5nprm  13221  dec2nprm  13222  modxai  13223  modxp1i  13225  mod2xnegi  13226  modsubi  13227  gcdmodi  13229  decsplit0b  13234  decsplit1  13236  decsplit  13237  karatsuba  13238  2exp7  13242  2exp8  13243  3exp3  13246  5prm  13251  7prm  13253  11prm  13257  prmlem2  13262  37prm  13263  43prm  13264  83prm  13265  139prm  13266  163prm  13267  317prm  13268  631prm  13269  1259lem1  13270  1259lem2  13271  1259lem3  13272  1259lem4  13273  1259lem5  13274  ballotfilem1  13277  ballotfilem2  13285  ballotfilemi1  13302  ballotfilemii  13303  ballotfilemic  13307  ballotfilem1c  13308  ballotfilemfrceq  13329  ballotfilemth  13338  subsubm  13848  mulg2  13992  subsubg  14058  gsumconstcmn  14265  pwsbas  14311  unitsubm  14534  subsubrng  14630  subsubrg  14661  lsslss  14826  expghmap  15050  cnmpt1res  15539  rerestcntop  15801  rerest  15803  dvfvalap  15924  dvcnp2cntop  15942  dveflem  15969  plyun0  15979  dvply1  16008  reeff1oleme  16015  sin0pilem1  16025  sinhalfpilem  16035  cospi  16044  eulerid  16046  cos2pi  16048  ef2kpi  16050  sinhalfpip  16064  sinhalfpim  16065  coshalfpip  16066  coshalfpim  16067  sincosq3sgn  16072  sincosq4sgn  16073  cosq23lt0  16077  tangtx  16082  sincos4thpi  16084  sincos6thpi  16086  sineq0re  16093  cosq34lt1  16095  logfac  16143  rplogb1  16201  2logb9irr  16224  sqrt2cxp2logb9e3  16228  2logb9irrap  16230  binom4  16236  log2tlbndlog2  16237  log2ublem2  16239  log2ublem3  16240  log2ublog2  16241  birthdaylog2  16245  ppi1i  16289  ppiublem1  16308  ppiqub  16310  chtublem  16312  chtqub  16313  bclbnd  16324  bposlem6  16333  bposlem8  16335  bposlem9  16336  lgsdir2lem1  16369  lgsdir2lem2  16370  lgsdir2lem4  16372  lgsdir2lem5  16373  lgsne0  16379  1lgs  16384  gausslemma2dlem0e  16394  gausslemma2dlem0f  16395  gausslemma2dlem3  16404  gausslemma2d  16410  lgseisenlem1  16411  lgseisenlem2  16412  lgseisenlem3  16413  lgseisenlem4  16414  lgseisen  16415  lgsquadlem1  16418  lgsquadlem2  16419  lgsquad2lem1  16422  lgsquad2lem2  16423  m1lgs  16426  2lgslem3a  16434  2lgslem3b  16435  2lgslem3c  16436  2lgslem3d  16437  2lgsoddprmlem3a  16448  2lgsoddprmlem3b  16449  2lgsoddprmlem3c  16450  2lgsoddprmlem3d  16451  ex-fl  16961  ex-exp  16963  ex-bc  16965  depindlem1  16969  012of  17245  2o01f  17246  qdencn  17295  isomninnlem  17302  iswomninnlem  17323  ismkvnnlem  17326