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  6745  nnm1  6803  nnm2  6804  mapsnconst  6982  mapsncnv  6983  exmidpw2en  7225  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  9689  nn0n0n1ge2  9724  nneoor  9758  zeo  9761  numsuc  9800  numltc  9817  numsucc  9831  numma  9835  nummul1c  9840  decrmac  9849  decsubi  9854  decmul1  9855  decmul10add  9860  6p5lem  9861  5p5e10  9862  6p4e10  9863  7p3e10  9866  8p2e10  9871  4t3lem  9888  9t11e99  9921  decbin2  9932  fz00m1  10467  fztp  10501  fzprval  10505  fztpval  10506  fzshftral  10531  fz0tp  10545  fz0to3un2pr  10546  fzo01  10650  fzo12sn  10651  fzo0to2pr  10652  fzo0to3tp  10653  fzo0to42pr  10654  intqfrac2  10776  intfracq  10777  xnn0nnen  10894  sqval  11054  sq4e2t8  11094  cu2  11095  i3  11098  i4  11099  binom2i  11105  binom3  11114  3dec  11173  faclbnd  11200  faclbnd2  11201  bcn1  11217  bcn2  11223  4bc3eq4  11233  4bc2eq6  11234  hashmap  11289  hashfibclem  11303  ccatlid  11395  ccatrid  11396  pfx1  11496  pfxccatin12lem3  11525  pfxccatpfx1  11529  pfxccatpfx2  11530  cats1fvn  11557  cats1catd  11561  cats2catd  11562  reim0  11647  cji  11689  resqrexlemover  11797  resqrexlemcalc1  11801  resqrexlemcalc3  11803  absi  11846  fsump1i  12224  fsumconst  12245  modfsummodlemstep  12248  arisum2  12290  geoihalfsum  12313  mertenslemi1  12326  mertenslem2  12327  mertensabs  12328  fprodconst  12411  fprodrec  12420  ef0lem  12451  ege2le3  12462  eft0val  12484  ef4p  12485  efgt1p2  12486  efgt1p  12487  tanval2ap  12504  efival  12523  ef01bndlem  12547  sin01bnd  12548  cos01bnd  12549  cos1bnd  12550  cos2bnd  12551  3dvdsdec  12656  3dvds2dec  12657  odd2np1lem  12663  odd2np1  12664  oddp1even  12667  mod2eq1n2dvds  12670  opoe  12686  bits0  12739  0bits  12750  6gcd4e2  12796  lcmneg  12876  3lcm2e6woprm  12888  6lcm4e12  12889  3prm  12930  3lcm2e6  12963  sqrt2irrlem  12964  pwbdvdslemn  12968  phiprm  13029  prmdiv  13041  pythagtriplem12  13082  pythagtriplem14  13084  pcfac  13157  prmpwdvds  13162  pockthi  13165  4sqlem5  13189  4sqlem13m  13210  modxai  13223  mod2xnegi  13226  gcdi  13228  numexpp1  13232  numexp2x  13233  decsplit0b  13234  decsplit1  13236  decsplit  13237  2exp5  13240  2exp7  13242  2exp11  13244  2exp16  13245  prmlem0  13248  139prm  13266  163prm  13267  317prm  13268  631prm  13269  1259lem4  13273  1259lem5  13274  1259prm  13275  ballotfilem2  13285  ballotfilemth  13338  ressval2  13478  ecqusaddd  14099  gzsumconstf  14233  gsumzfi  14247  gsumclfi  14248  gsummptfidmadd  14250  gsumsubmclfi  14252  gsummptfidmsplit  14253  gsummptfidmsplitres  14254  gsumsnfdcmn  14256  gsumresfi  14262  gsummhmfi  14263  gsumconstcmn  14265  gsum2dfilem2  14271  gsumfsum  15031  znbas  15087  znzrh2  15089  restin  15419  uptx  15517  cnrehmeocntop  15853  hoverb  15891  dvexp  15954  dvmptidcn  15957  dvmptccn  15958  dvmptid  15959  dvmptc  15960  dvmptfsum  15968  dveflem  15969  plymullem1  15991  sinhalfpilem  16035  efhalfpi  16043  cospi  16044  efipi  16045  sin2pi  16047  cos2pi  16048  ef2pi  16049  sin2pim  16057  cos2pim  16058  sinmpi  16059  cosmpi  16060  sinppi  16061  cosppi  16062  sincosq4sgn  16073  tangtx  16082  sincos4thpi  16084  sincos6thpi  16086  sincos3rdpi  16087  abssinper  16090  cosq34lt1  16095  logfac  16143  1cxp  16150  ecxp  16151  rpcxpsqrt  16174  rpelogb  16202  2logb9irrALT  16227  zprmlogbaplem2  16233  binom4  16236  log2tlbndlog2  16237  log2ublem1  16238  log2ublem2  16239  log2ublem3  16240  log2ublog2  16241  birthdaylog2  16245  cht1  16288  1sgmprm  16305  ppiublem2  16309  ppiqub  16310  chtublem  16312  chtqub  16313  bcp1ctr  16323  bclbnd  16324  bposlem4  16331  bposlem6  16333  bposlem8  16335  bposlem9  16336  lgslem1  16341  lgsdir2lem1  16369  lgsdir2lem2  16370  lgsdir2lem3  16371  lgsdir2lem5  16373  lgs1  16385  gausslemma2dlem1a  16399  gausslemma2dlem3  16404  gausslemma2dlem4  16405  gausslemma2d  16410  lgseisenlem1  16411  lgseisenlem3  16413  lgsquadlem1  16418  lgsquadlem2  16419  lgsquad2lem2  16423  m1lgs  16426  2lgslem1a2  16428  2sqlem8  16464  setsiedg  16515  vdegp1cid  16779  clwwlknonex2lem1  16900  ex-exp  16963  ex-bc  16965  ex-gcd  16967  cvgcmp2nlemabs  17304