Theorem oveq1i 6095

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 6092	. 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 6085

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 4131  df-iota 5337  df-fv 5385  df-ov 6088

This theorem is used by:  caov12  6278  map1  7101  exmidpw2en  7219  halfnqq  7777  prarloclem5  7867  m1m1sr  8128  caucvgsrlemfv  8158  caucvgsr  8169  pitonnlem1  8212  axi2m1  8242  axcnre  8248  axcaucvg  8267  mvrraddi  8544  mvlladdi  8545  negsubdi  8583  mul02  8715  mulneg1  8723  mulreim  8934  recextlem1  8981  recdivap  9050  2p2e4  9433  2times  9434  3p2e5  9448  3p3e6  9449  4p2e6  9450  4p3e7  9451  4p4e8  9452  5p2e7  9453  5p3e8  9454  5p4e9  9455  6p2e8  9456  6p3e9  9457  7p2e9  9458  1mhlfehlf  9527  8th4div3  9528  halfpm6th  9529  nneoor  9752  9p1e10  9783  dfdec10  9784  num0h  9792  numsuc  9794  dec10p  9828  numma  9829  nummac  9830  numma2c  9831  numadd  9832  numaddc  9833  nummul2c  9835  decaddci  9846  decsubi  9848  decmul1  9849  5p5e10  9856  6p4e10  9857  7p3e10  9860  8p2e10  9865  decbin0  9925  decbin2  9926  elfzp1b  10514  elfzm1b  10515  fz01or  10528  fz1ssfz0  10534  fz0to4untppr  10541  qbtwnrelemcalc  10700  fldiv4p1lem1div2  10753  1tonninf  10891  mulexpzap  11029  expaddzap  11033  sq4e2t8  11087  cu2  11088  i3  11091  iexpcyc  11094  binom2i  11098  binom3  11107  3dec  11166  faclbnd  11193  bcm1k  11212  bcp1nk  11214  bcpasc  11218  hashp1i  11265  hashxp  11281  hashpwfi  11283  hashfibc  11297  ccatlid  11388  pfxccatin12lem2c  11516  imre  11630  crim  11637  remullem  11650  sq01  11674  resqrexlemfp1  11789  resqrexlemover  11790  resqrexlemcalc1  11794  resqrexlemnm  11798  absexpzap  11861  absimle  11865  amgm2  11899  maxabslemlub  11988  fsumconst  12237  modfsummod  12241  binomlem  12266  binom11  12269  arisum  12281  arisum2  12282  georeclim  12296  geo2sum  12297  mertenslemi1  12318  mertenslem2  12319  mertensabs  12320  prodfrecap  12329  fprodm1s  12384  fprodp1s  12385  fprodrec  12412  fprodmodd  12424  efzval  12466  resinval  12498  recosval  12499  efi4p  12500  tan0  12514  efival  12515  cosadd  12520  cos2tsin  12534  ef01bndlem  12539  cos1bnd  12542  cos2bnd  12543  absefib  12554  efieq1re  12555  demoivreALT  12557  eirraplem  12560  3dvds  12647  3dvdsdec  12648  3dvds2dec  12649  odd2np1  12656  nn0o1gt2  12688  nn0o  12690  5ndvds3  12717  5ndvds6  12718  flodddiv4  12719  m1bits  12743  algrp1  12840  3lcm2e6woprm  12880  nn0gcdsq  12996  phiprmpw  13020  prmdiv  13033  prmdiveq  13034  pythagtriplem1  13064  pythagtriplem12  13074  pythagtriplem14  13076  pockthi  13157  infpnlem1  13158  4sqlem12  13201  4sqlem13m  13202  4sqlem19  13208  dec5dvds  13211  dec5nprm  13213  dec2nprm  13214  modxai  13215  modxp1i  13217  mod2xnegi  13218  modsubi  13219  gcdmodi  13221  decsplit0b  13226  decsplit1  13228  decsplit  13229  karatsuba  13230  2exp7  13234  2exp8  13235  3exp3  13238  5prm  13243  7prm  13245  11prm  13249  prmlem2  13254  37prm  13255  43prm  13256  83prm  13257  139prm  13258  163prm  13259  317prm  13260  631prm  13261  1259lem1  13262  1259lem2  13263  1259lem3  13264  1259lem4  13265  1259lem5  13266  ballotfilem1  13269  ballotfilem2  13277  ballotfilemi1  13294  ballotfilemii  13295  ballotfilemic  13299  ballotfilem1c  13300  ballotfilemfrceq  13321  ballotfilemth  13330  subsubm  13839  mulg2  13983  subsubg  14049  gsumconstcmn  14215  pwsbas  14254  unitsubm  14475  subsubrng  14571  subsubrg  14602  lsslss  14767  expghmap  14991  cnmpt1res  15446  rerestcntop  15708  rerest  15710  dvfvalap  15831  dvcnp2cntop  15849  dveflem  15876  plyun0  15886  dvply1  15915  reeff1oleme  15922  sin0pilem1  15932  sinhalfpilem  15942  cospi  15951  eulerid  15953  cos2pi  15955  ef2kpi  15957  sinhalfpip  15971  sinhalfpim  15972  coshalfpip  15973  coshalfpim  15974  sincosq3sgn  15979  sincosq4sgn  15980  cosq23lt0  15984  tangtx  15989  sincos4thpi  15991  sincos6thpi  15993  cosq34lt1  16001  logfac  16048  rplogb1  16103  2logb9irr  16126  sqrt2cxp2logb9e3  16130  2logb9irrap  16132  binom4  16138  log2tlbndlog2  16139  log2ublem2  16141  log2ublem3  16142  log2ublog2  16143  birthdaylog2  16147  ppi1i  16177  ppiublem1  16192  ppiqub  16194  bclbnd  16205  lgsdir2lem1  16245  lgsdir2lem2  16246  lgsdir2lem4  16248  lgsdir2lem5  16249  lgsne0  16255  1lgs  16260  gausslemma2dlem0e  16270  gausslemma2dlem0f  16271  gausslemma2dlem3  16280  gausslemma2d  16286  lgseisenlem1  16287  lgseisenlem2  16288  lgseisenlem3  16289  lgseisenlem4  16290  lgseisen  16291  lgsquadlem1  16294  lgsquadlem2  16295  lgsquad2lem1  16298  lgsquad2lem2  16299  m1lgs  16302  2lgslem3a  16310  2lgslem3b  16311  2lgslem3c  16312  2lgslem3d  16313  2lgsoddprmlem3a  16324  2lgsoddprmlem3b  16325  2lgsoddprmlem3c  16326  2lgsoddprmlem3d  16327  ex-fl  16837  ex-exp  16839  ex-bc  16841  depindlem1  16845  012of  17121  2o01f  17122  qdencn  17170  isomninnlem  17177  iswomninnlem  17197  ismkvnnlem  17200