Theorem oveq2i 6099

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

Hypothesis

Ref	Expression
oveq1i.1	⊢ 𝐴 = 𝐵

Assertion

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

Proof of Theorem oveq2i

Step	Hyp	Ref	Expression
1		oveq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		oveq2 6096	. 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:  caov32  6280  oa1suc  6744  nnm1  6802  nnm2  6803  mapsnconst  6980  mapsncnv  6981  exmidpw2en  7223  mulidnq  7762  halfnqq  7783  addpinq1  7837  addnqpr1  7935  caucvgprlemm  8041  caucvgprprlemval  8061  caucvgprprlemnbj  8066  caucvgprprlemmu  8068  caucvgprprlemaddq  8081  caucvgprprlem1  8082  caucvgprprlem2  8083  m1p1sr  8133  m1m1sr  8134  0idsr  8140  1idsr  8141  00sr  8142  pn0sr  8144  ltm1sr  8150  caucvgsrlemoffres  8173  caucvgsr  8175  mulresr  8211  pitonnlem2  8220  axi2m1  8248  ax1rid  8250  axcnre  8254  add42i  8499  negid  8580  negsub  8581  subneg  8582  negsubdii  8618  apreap  8923  recexaplem2  8988  muleqadd  9006  crap0  9296  2p2e4  9440  3p2e5  9455  3p3e6  9456  4p2e6  9457  4p3e7  9458  4p4e8  9459  5p2e7  9460  5p3e8  9461  5p4e9  9462  6p2e8  9463  6p3e9  9464  7p2e9  9465  3t3e9  9472  8th4div3  9535  halfpm6th  9536  iap0  9539  addltmul  9553  div4p1lem1div2  9570  peano2z  9691  nn0n0n1ge2  9726  nneoor  9759  zeo  9762  numsuc  9801  numltc  9818  numsucc  9832  numma  9836  nummul1c  9841  decrmac  9850  decsubi  9855  decmul1  9856  decmul10add  9861  6p5lem  9862  5p5e10  9863  6p4e10  9864  7p3e10  9867  8p2e10  9872  4t3lem  9889  9t11e99  9922  decbin2  9933  fz00m1  10468  fztp  10502  fzprval  10506  fztpval  10507  fzshftral  10532  fz0tp  10546  fz0to3un2pr  10547  fzo01  10651  fzo12sn  10652  fzo0to2pr  10653  fzo0to3tp  10654  fzo0to42pr  10655  intqfrac2  10777  intfracq  10778  xnn0nnen  10895  sqval  11055  sq4e2t8  11095  cu2  11096  i3  11099  i4  11100  binom2i  11106  binom3  11115  3dec  11174  faclbnd  11201  faclbnd2  11202  bcn1  11218  bcn2  11224  4bc3eq4  11234  4bc2eq6  11235  hashmap  11290  hashfibclem  11304  ccatlid  11396  ccatrid  11397  pfx1  11497  pfxccatin12lem3  11526  pfxccatpfx1  11530  pfxccatpfx2  11531  cats1fvn  11558  cats1catd  11562  cats2catd  11563  reim0  11648  cji  11690  resqrexlemover  11798  resqrexlemcalc1  11802  resqrexlemcalc3  11804  absi  11847  fsump1i  12225  fsumconst  12246  modfsummodlemstep  12249  arisum2  12291  geoihalfsum  12314  mertenslemi1  12327  mertenslem2  12328  mertensabs  12329  fprodconst  12412  fprodrec  12421  ef0lem  12452  ege2le3  12463  eft0val  12485  ef4p  12486  efgt1p2  12487  efgt1p  12488  tanval2ap  12505  efival  12524  ef01bndlem  12548  sin01bnd  12549  cos01bnd  12550  cos1bnd  12551  cos2bnd  12552  3dvdsdec  12657  3dvds2dec  12658  odd2np1lem  12664  odd2np1  12665  oddp1even  12668  mod2eq1n2dvds  12671  opoe  12687  bits0  12740  0bits  12751  6gcd4e2  12797  lcmneg  12877  3lcm2e6woprm  12889  6lcm4e12  12890  3prm  12931  3lcm2e6  12964  sqrt2irrlem  12965  pwbdvdslemn  12969  phiprm  13030  prmdiv  13042  pythagtriplem12  13083  pythagtriplem14  13085  pcfac  13158  prmpwdvds  13163  pockthi  13166  4sqlem5  13190  4sqlem13m  13211  modxai  13224  mod2xnegi  13227  gcdi  13229  numexpp1  13233  numexp2x  13234  decsplit0b  13235  decsplit1  13237  decsplit  13238  2exp5  13241  2exp7  13243  2exp11  13245  2exp16  13246  prmlem0  13249  139prm  13267  163prm  13268  317prm  13269  631prm  13270  1259lem4  13274  1259lem5  13275  1259prm  13276  ballotfilem2  13286  ballotfilemth  13339  ressval2  13479  ecqusaddd  14100  gzsumconstf  14234  gsumzfi  14248  gsumclfi  14249  gsummptfidmadd  14251  gsumsubmclfi  14253  gsummptfidmsplit  14254  gsummptfidmsplitres  14255  gsumsnfdcmn  14257  gsumresfi  14263  gsummhmfi  14264  gsumconstcmn  14266  gsum2dfilem2  14272  gsumfsum  15032  znbas  15088  znzrh2  15090  restin  15402  uptx  15500  cnrehmeocntop  15836  hoverb  15874  dvexp  15937  dvmptidcn  15940  dvmptccn  15941  dvmptid  15942  dvmptc  15943  dvmptfsum  15951  dveflem  15952  plymullem1  15974  sinhalfpilem  16018  efhalfpi  16026  cospi  16027  efipi  16028  sin2pi  16030  cos2pi  16031  ef2pi  16032  sin2pim  16040  cos2pim  16041  sinmpi  16042  cosmpi  16043  sinppi  16044  cosppi  16045  sincosq4sgn  16056  tangtx  16065  sincos4thpi  16067  sincos6thpi  16069  sincos3rdpi  16070  abssinper  16073  cosq34lt1  16078  logfac  16126  1cxp  16133  ecxp  16134  rpcxpsqrt  16157  rpelogb  16185  2logb9irrALT  16210  zprmlogbaplem2  16216  binom4  16219  log2tlbndlog2  16220  log2ublem1  16221  log2ublem2  16222  log2ublem3  16223  log2ublog2  16224  birthdaylog2  16228  cht1  16271  1sgmprm  16288  ppiublem2  16292  ppiqub  16293  chtublem  16295  chtqub  16296  bcp1ctr  16306  bclbnd  16307  bposlem4  16314  bposlem6  16316  bposlem8  16318  bposlem9  16319  lgslem1  16324  lgsdir2lem1  16352  lgsdir2lem2  16353  lgsdir2lem3  16354  lgsdir2lem5  16356  lgs1  16368  gausslemma2dlem1a  16382  gausslemma2dlem3  16387  gausslemma2dlem4  16388  gausslemma2d  16393  lgseisenlem1  16394  lgseisenlem3  16396  lgsquadlem1  16401  lgsquadlem2  16402  lgsquad2lem2  16406  m1lgs  16409  2lgslem1a2  16411  2sqlem8  16447  setsiedg  16498  vdegp1cid  16762  clwwlknonex2lem1  16883  ex-exp  16946  ex-bc  16948  ex-gcd  16950  cvgcmp2nlemabs  17287