Theorem oveq2i 6096

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 6093	. 2 |- ( A = B -> ( C F A ) = ( C F B ) )
3	1, 2	ax-mp 5	1 |- ( C F A ) = ( C F B )

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:  caov32  6277  oa1suc  6740  nnm1  6798  nnm2  6799  mapsnconst  6976  mapsncnv  6977  exmidpw2en  7219  mulidnq  7756  halfnqq  7777  addpinq1  7831  addnqpr1  7929  caucvgprlemm  8035  caucvgprprlemval  8055  caucvgprprlemnbj  8060  caucvgprprlemmu  8062  caucvgprprlemaddq  8075  caucvgprprlem1  8076  caucvgprprlem2  8077  m1p1sr  8127  m1m1sr  8128  0idsr  8134  1idsr  8135  00sr  8136  pn0sr  8138  ltm1sr  8144  caucvgsrlemoffres  8167  caucvgsr  8169  mulresr  8205  pitonnlem2  8214  axi2m1  8242  ax1rid  8244  axcnre  8248  add42i  8492  negid  8573  negsub  8574  subneg  8575  negsubdii  8611  apreap  8915  recexaplem2  8980  muleqadd  8998  crap0  9288  2p2e4  9431  3p2e5  9446  3p3e6  9447  4p2e6  9448  4p3e7  9449  4p4e8  9450  5p2e7  9451  5p3e8  9452  5p4e9  9453  6p2e8  9454  6p3e9  9455  7p2e9  9456  3t3e9  9462  8th4div3  9524  halfpm6th  9525  iap0  9528  addltmul  9542  div4p1lem1div2  9559  peano2z  9680  nn0n0n1ge2  9715  nneoor  9748  zeo  9751  numsuc  9790  numltc  9802  numsucc  9816  numma  9820  nummul1c  9825  decrmac  9834  decsubi  9839  decmul1  9840  decmul10add  9845  6p5lem  9846  5p5e10  9847  6p4e10  9848  7p3e10  9851  8p2e10  9856  4t3lem  9873  9t11e99  9906  decbin2  9917  fz00m1  10451  fztp  10485  fzprval  10489  fztpval  10490  fzshftral  10515  fz0tp  10529  fz0to3un2pr  10530  fzo01  10634  fzo12sn  10635  fzo0to2pr  10636  fzo0to3tp  10637  fzo0to42pr  10638  intqfrac2  10756  intfracq  10757  xnn0nnen  10874  sqval  11034  sq4e2t8  11074  cu2  11075  i3  11078  i4  11079  binom2i  11085  binom3  11094  3dec  11152  faclbnd  11179  faclbnd2  11180  bcn1  11196  bcn2  11202  4bc3eq4  11212  4bc2eq6  11213  hashmap  11268  hashfibclem  11282  ccatlid  11374  ccatrid  11375  pfx1  11475  pfxccatin12lem3  11504  pfxccatpfx1  11508  pfxccatpfx2  11509  cats1fvn  11536  cats1catd  11540  cats2catd  11541  reim0  11626  cji  11668  resqrexlemover  11776  resqrexlemcalc1  11780  resqrexlemcalc3  11782  absi  11825  fsump1i  12200  fsumconst  12221  modfsummodlemstep  12224  arisum2  12266  geoihalfsum  12289  mertenslemi1  12302  mertenslem2  12303  mertensabs  12304  fprodconst  12387  fprodrec  12396  ef0lem  12427  ege2le3  12438  eft0val  12460  ef4p  12461  efgt1p2  12462  efgt1p  12463  tanval2ap  12480  efival  12499  ef01bndlem  12523  sin01bnd  12524  cos01bnd  12525  cos1bnd  12526  cos2bnd  12527  3dvdsdec  12632  3dvds2dec  12633  odd2np1lem  12639  odd2np1  12640  oddp1even  12643  mod2eq1n2dvds  12646  opoe  12662  bits0  12715  0bits  12726  6gcd4e2  12772  lcmneg  12852  3lcm2e6woprm  12864  6lcm4e12  12865  3prm  12906  3lcm2e6  12938  sqrt2irrlem  12939  pw2dvdslemn  12943  phiprm  13001  prmdiv  13013  pythagtriplem12  13054  pythagtriplem14  13056  pcfac  13129  prmpwdvds  13134  pockthi  13137  4sqlem5  13161  4sqlem13m  13182  modxai  13195  gcdi  13199  numexpp1  13203  numexp2x  13204  decsplit0b  13205  decsplit1  13207  decsplit  13208  2exp5  13211  2exp7  13213  2exp11  13215  2exp16  13216  ballotfilem2  13228  ballotfilemth  13281  ressval2  13420  ecqusaddd  14041  gzsumconstf  14144  gsumzfi  14158  gsumclfi  14159  gsummptfidmadd  14161  gsumsubmclfi  14163  gsummhmfi  14164  gsumconstcmn  14166  gsumfsum  14923  znbas  14979  znzrh2  14981  restin  15277  uptx  15375  cnrehmeocntop  15711  hoverb  15749  dvexp  15812  dvmptidcn  15815  dvmptccn  15816  dvmptid  15817  dvmptc  15818  dvmptfsum  15826  dveflem  15827  plymullem1  15849  sinhalfpilem  15892  efhalfpi  15900  cospi  15901  efipi  15902  sin2pi  15904  cos2pi  15905  ef2pi  15906  sin2pim  15914  cos2pim  15915  sinmpi  15916  cosmpi  15917  sinppi  15918  cosppi  15919  sincosq4sgn  15930  tangtx  15939  sincos4thpi  15941  sincos6thpi  15943  sincos3rdpi  15944  abssinper  15947  cosq34lt1  15951  logfac  15995  1cxp  16002  ecxp  16003  rpcxpsqrt  16024  rpelogb  16051  2logb9irrALT  16076  binom4  16081  log2tlbndlog2  16082  log2ublem1  16083  log2ublem2  16084  log2ublem3  16085  log2ublog2  16086  birthdaylog2  16090  1sgmprm  16108  lgslem1  16119  lgsdir2lem1  16147  lgsdir2lem2  16148  lgsdir2lem3  16149  lgsdir2lem5  16151  lgs1  16163  gausslemma2dlem1a  16177  gausslemma2dlem3  16182  gausslemma2dlem4  16183  gausslemma2d  16188  lgseisenlem1  16189  lgseisenlem3  16191  lgsquadlem1  16196  lgsquadlem2  16197  lgsquad2lem2  16201  m1lgs  16204  2lgslem1a2  16206  2sqlem8  16242  setsiedg  16293  vdegp1cid  16557  clwwlknonex2lem1  16678  ex-exp  16741  ex-bc  16743  ex-gcd  16745  cvgcmp2nlemabs  17081