Theorem oveq2i 5793

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

Hypothesis

Ref	Expression
oveq1i.1	|- A = B

Assertion

Ref	Expression
oveq2i	|- ( C F A ) = ( C F B )

Proof of Theorem oveq2i

Step	Hyp	Ref	Expression
1		oveq1i.1	. 2 |- A = B
2		oveq2 5790	. 2 |- ( A = B -> ( C F A ) = ( C F B ) )
3	1, 2	ax-mp 5	1 |- ( C F A ) = ( C F B )

Syntax hints:   = wceq 1332  (class class class)co 5782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rex 2423  df-v 2691  df-un 3080  df-sn 3538  df-pr 3539  df-op 3541  df-uni 3745  df-br 3938  df-iota 5096  df-fv 5139  df-ov 5785

This theorem is referenced by:  caov32  5966  oa1suc  6371  nnm1  6428  nnm2  6429  mapsnconst  6596  mapsncnv  6597  mulidnq  7221  halfnqq  7242  addpinq1  7296  addnqpr1  7394  caucvgprlemm  7500  caucvgprprlemval  7520  caucvgprprlemnbj  7525  caucvgprprlemmu  7527  caucvgprprlemaddq  7540  caucvgprprlem1  7541  caucvgprprlem2  7542  m1p1sr  7592  m1m1sr  7593  0idsr  7599  1idsr  7600  00sr  7601  pn0sr  7603  ltm1sr  7609  caucvgsrlemoffres  7632  caucvgsr  7634  mulresr  7670  pitonnlem2  7679  axi2m1  7707  ax1rid  7709  axcnre  7713  add42i  7952  negid  8033  negsub  8034  subneg  8035  negsubdii  8071  apreap  8373  recexaplem2  8437  muleqadd  8453  crap0  8740  2p2e4  8871  3p2e5  8885  3p3e6  8886  4p2e6  8887  4p3e7  8888  4p4e8  8889  5p2e7  8890  5p3e8  8891  5p4e9  8892  6p2e8  8893  6p3e9  8894  7p2e9  8895  3t3e9  8901  8th4div3  8963  halfpm6th  8964  iap0  8967  addltmul  8980  div4p1lem1div2  8997  peano2z  9114  nn0n0n1ge2  9145  nneoor  9177  zeo  9180  numsuc  9219  numltc  9231  numsucc  9245  numma  9249  nummul1c  9254  decrmac  9263  decsubi  9268  decmul1  9269  decmul10add  9274  6p5lem  9275  5p5e10  9276  6p4e10  9277  7p3e10  9280  8p2e10  9285  4t3lem  9302  9t11e99  9335  decbin2  9346  fztp  9889  fzprval  9893  fztpval  9894  fzshftral  9919  fz0tp  9932  fzo01  10024  fzo12sn  10025  fzo0to2pr  10026  fzo0to3tp  10027  fzo0to42pr  10028  intqfrac2  10123  intfracq  10124  sqval  10382  sq4e2t8  10421  cu2  10422  i3  10425  i4  10426  binom2i  10432  binom3  10440  3dec  10492  faclbnd  10519  faclbnd2  10520  bcn1  10536  bcn2  10542  4bc3eq4  10551  4bc2eq6  10552  reim0  10665  cji  10706  resqrexlemover  10814  resqrexlemcalc1  10818  resqrexlemcalc3  10820  absi  10863  fsump1i  11234  fsumconst  11255  modfsummodlemstep  11258  arisum2  11300  geoihalfsum  11323  mertenslemi1  11336  mertenslem2  11337  mertensabs  11338  ef0lem  11403  ege2le3  11414  eft0val  11436  ef4p  11437  efgt1p2  11438  efgt1p  11439  tanval2ap  11456  efival  11475  ef01bndlem  11499  sin01bnd  11500  cos01bnd  11501  cos1bnd  11502  cos2bnd  11503  3dvdsdec  11598  3dvds2dec  11599  odd2np1lem  11605  odd2np1  11606  oddp1even  11609  mod2eq1n2dvds  11612  opoe  11628  6gcd4e2  11719  lcmneg  11791  3lcm2e6woprm  11803  6lcm4e12  11804  3prm  11845  3lcm2e6  11874  sqrt2irrlem  11875  pw2dvdslemn  11879  phiprm  11935  restin  12384  uptx  12482  cnrehmeocntop  12801  dvexp  12883  dvmptidcn  12886  dvmptccn  12887  dveflem  12895  sinhalfpilem  12920  efhalfpi  12928  cospi  12929  efipi  12930  sin2pi  12932  cos2pi  12933  ef2pi  12934  sin2pim  12942  cos2pim  12943  sinmpi  12944  cosmpi  12945  sinppi  12946  cosppi  12947  sincosq4sgn  12958  tangtx  12967  sincos4thpi  12969  sincos6thpi  12971  sincos3rdpi  12972  abssinper  12975  cosq34lt1  12979  1cxp  13029  ecxp  13030  rpcxpsqrt  13050  rpelogb  13074  2logb9irrALT  13099  ex-exp  13110  ex-bc  13112  ex-gcd  13114  cvgcmp2nlemabs  13402