Theorem oveq1i 6098

Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)

Hypothesis

Ref	Expression
oveq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
oveq1i	⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐶)

Proof of Theorem oveq1i

Step	Hyp	Ref	Expression
1		oveq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		oveq1 6095	. 2 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐶)

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  7105  exmidpw2en  7223  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  9759  9p1e10  9790  dfdec10  9791  num0h  9799  numsuc  9801  dec10p  9835  numma  9836  nummac  9837  numma2c  9838  numadd  9839  numaddc  9840  nummul2c  9842  decaddci  9853  decsubi  9855  decmul1  9856  5p5e10  9863  6p4e10  9864  7p3e10  9867  8p2e10  9872  decbin0  9932  decbin2  9933  elfzp1b  10521  elfzm1b  10522  fz01or  10535  fz1ssfz0  10541  fz0to4untppr  10548  qbtwnrelemcalc  10707  fldiv4p1lem1div2  10761  1tonninf  10899  mulexpzap  11037  expaddzap  11041  sq4e2t8  11095  cu2  11096  i3  11099  iexpcyc  11102  binom2i  11106  binom3  11115  3dec  11174  faclbnd  11201  bcm1k  11220  bcp1nk  11222  bcpasc  11226  hashp1i  11273  hashxp  11289  hashpwfi  11291  hashfibc  11305  ccatlid  11396  pfxccatin12lem2c  11524  imre  11638  crim  11645  remullem  11658  sq01  11682  resqrexlemfp1  11797  resqrexlemover  11798  resqrexlemcalc1  11802  resqrexlemnm  11806  absexpzap  11869  absimle  11873  amgm2  11907  maxabslemlub  11996  fsumconst  12246  modfsummod  12250  binomlem  12275  binom11  12278  arisum  12290  arisum2  12291  georeclim  12305  geo2sum  12306  mertenslemi1  12327  mertenslem2  12328  mertensabs  12329  prodfrecap  12338  fprodm1s  12393  fprodp1s  12394  fprodrec  12421  fprodmodd  12433  efzval  12475  resinval  12507  recosval  12508  efi4p  12509  tan0  12523  efival  12524  cosadd  12529  cos2tsin  12543  ef01bndlem  12548  cos1bnd  12551  cos2bnd  12552  absefib  12563  efieq1re  12564  demoivreALT  12566  eirraplem  12569  3dvds  12656  3dvdsdec  12657  3dvds2dec  12658  odd2np1  12665  nn0o1gt2  12697  nn0o  12699  5ndvds3  12726  5ndvds6  12727  flodddiv4  12728  m1bits  12752  algrp1  12849  3lcm2e6woprm  12889  nn0gcdsq  13005  phiprmpw  13029  prmdiv  13042  prmdiveq  13043  pythagtriplem1  13073  pythagtriplem12  13083  pythagtriplem14  13085  pockthi  13166  infpnlem1  13167  4sqlem12  13210  4sqlem13m  13211  4sqlem19  13217  dec5dvds  13220  dec5nprm  13222  dec2nprm  13223  modxai  13224  modxp1i  13226  mod2xnegi  13227  modsubi  13228  gcdmodi  13230  decsplit0b  13235  decsplit1  13237  decsplit  13238  karatsuba  13239  2exp7  13243  2exp8  13244  3exp3  13247  5prm  13252  7prm  13254  11prm  13258  prmlem2  13263  37prm  13264  43prm  13265  83prm  13266  139prm  13267  163prm  13268  317prm  13269  631prm  13270  1259lem1  13271  1259lem2  13272  1259lem3  13273  1259lem4  13274  1259lem5  13275  ballotfilem1  13278  ballotfilem2  13286  ballotfilemi1  13303  ballotfilemii  13304  ballotfilemic  13308  ballotfilem1c  13309  ballotfilemfrceq  13330  ballotfilemth  13339  subsubm  13849  mulg2  13993  subsubg  14059  gsumconstcmn  14266  pwsbas  14312  unitsubm  14535  subsubrng  14631  subsubrg  14662  lsslss  14827  expghmap  15051  cnmpt1res  15522  rerestcntop  15784  rerest  15786  dvfvalap  15907  dvcnp2cntop  15925  dveflem  15952  plyun0  15962  dvply1  15991  reeff1oleme  15998  sin0pilem1  16008  sinhalfpilem  16018  cospi  16027  eulerid  16029  cos2pi  16031  ef2kpi  16033  sinhalfpip  16047  sinhalfpim  16048  coshalfpip  16049  coshalfpim  16050  sincosq3sgn  16055  sincosq4sgn  16056  cosq23lt0  16060  tangtx  16065  sincos4thpi  16067  sincos6thpi  16069  sineq0re  16076  cosq34lt1  16078  logfac  16126  rplogb1  16184  2logb9irr  16207  sqrt2cxp2logb9e3  16211  2logb9irrap  16213  binom4  16219  log2tlbndlog2  16220  log2ublem2  16222  log2ublem3  16223  log2ublog2  16224  birthdaylog2  16228  ppi1i  16272  ppiublem1  16291  ppiqub  16293  chtublem  16295  chtqub  16296  bclbnd  16307  bposlem6  16316  bposlem8  16318  bposlem9  16319  lgsdir2lem1  16352  lgsdir2lem2  16353  lgsdir2lem4  16355  lgsdir2lem5  16356  lgsne0  16362  1lgs  16367  gausslemma2dlem0e  16377  gausslemma2dlem0f  16378  gausslemma2dlem3  16387  gausslemma2d  16393  lgseisenlem1  16394  lgseisenlem2  16395  lgseisenlem3  16396  lgseisenlem4  16397  lgseisen  16398  lgsquadlem1  16401  lgsquadlem2  16402  lgsquad2lem1  16405  lgsquad2lem2  16406  m1lgs  16409  2lgslem3a  16417  2lgslem3b  16418  2lgslem3c  16419  2lgslem3d  16420  2lgsoddprmlem3a  16431  2lgsoddprmlem3b  16432  2lgsoddprmlem3c  16433  2lgsoddprmlem3d  16434  ex-fl  16944  ex-exp  16946  ex-bc  16948  depindlem1  16952  012of  17228  2o01f  17229  qdencn  17278  isomninnlem  17285  iswomninnlem  17306  ismkvnnlem  17309