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  8493  negid  8574  negsub  8575  subneg  8576  negsubdii  8612  apreap  8917  recexaplem2  8982  muleqadd  9000  crap0  9290  2p2e4  9433  3p2e5  9448  3p3e6  9449  4p2e6  9450  4p3e7  9451  4p4e8  9452  5p2e7  9453  5p3e8  9454  5p4e9  9455  6p2e8  9456  6p3e9  9457  7p2e9  9458  3t3e9  9465  8th4div3  9528  halfpm6th  9529  iap0  9532  addltmul  9546  div4p1lem1div2  9563  peano2z  9684  nn0n0n1ge2  9719  nneoor  9752  zeo  9755  numsuc  9794  numltc  9811  numsucc  9825  numma  9829  nummul1c  9834  decrmac  9843  decsubi  9848  decmul1  9849  decmul10add  9854  6p5lem  9855  5p5e10  9856  6p4e10  9857  7p3e10  9860  8p2e10  9865  4t3lem  9882  9t11e99  9915  decbin2  9926  fz00m1  10461  fztp  10495  fzprval  10499  fztpval  10500  fzshftral  10525  fz0tp  10539  fz0to3un2pr  10540  fzo01  10644  fzo12sn  10645  fzo0to2pr  10646  fzo0to3tp  10647  fzo0to42pr  10648  intqfrac2  10769  intfracq  10770  xnn0nnen  10887  sqval  11047  sq4e2t8  11087  cu2  11088  i3  11091  i4  11092  binom2i  11098  binom3  11107  3dec  11166  faclbnd  11193  faclbnd2  11194  bcn1  11210  bcn2  11216  4bc3eq4  11226  4bc2eq6  11227  hashmap  11282  hashfibclem  11296  ccatlid  11388  ccatrid  11389  pfx1  11489  pfxccatin12lem3  11518  pfxccatpfx1  11522  pfxccatpfx2  11523  cats1fvn  11550  cats1catd  11554  cats2catd  11555  reim0  11640  cji  11682  resqrexlemover  11790  resqrexlemcalc1  11794  resqrexlemcalc3  11796  absi  11839  fsump1i  12216  fsumconst  12237  modfsummodlemstep  12240  arisum2  12282  geoihalfsum  12305  mertenslemi1  12318  mertenslem2  12319  mertensabs  12320  fprodconst  12403  fprodrec  12412  ef0lem  12443  ege2le3  12454  eft0val  12476  ef4p  12477  efgt1p2  12478  efgt1p  12479  tanval2ap  12496  efival  12515  ef01bndlem  12539  sin01bnd  12540  cos01bnd  12541  cos1bnd  12542  cos2bnd  12543  3dvdsdec  12648  3dvds2dec  12649  odd2np1lem  12655  odd2np1  12656  oddp1even  12659  mod2eq1n2dvds  12662  opoe  12678  bits0  12731  0bits  12742  6gcd4e2  12788  lcmneg  12868  3lcm2e6woprm  12880  6lcm4e12  12881  3prm  12922  3lcm2e6  12955  sqrt2irrlem  12956  pwbdvdslemn  12960  phiprm  13021  prmdiv  13033  pythagtriplem12  13074  pythagtriplem14  13076  pcfac  13149  prmpwdvds  13154  pockthi  13157  4sqlem5  13181  4sqlem13m  13202  modxai  13215  mod2xnegi  13218  gcdi  13220  numexpp1  13224  numexp2x  13225  decsplit0b  13226  decsplit1  13228  decsplit  13229  2exp5  13232  2exp7  13234  2exp11  13236  2exp16  13237  prmlem0  13240  139prm  13258  163prm  13259  317prm  13260  631prm  13261  1259lem4  13265  1259lem5  13266  1259prm  13267  ballotfilem2  13277  ballotfilemth  13330  ressval2  13469  ecqusaddd  14090  gzsumconstf  14193  gsumzfi  14207  gsumclfi  14208  gsummptfidmadd  14210  gsumsubmclfi  14212  gsummhmfi  14213  gsumconstcmn  14215  gsumfsum  14972  znbas  15028  znzrh2  15030  restin  15326  uptx  15424  cnrehmeocntop  15760  hoverb  15798  dvexp  15861  dvmptidcn  15864  dvmptccn  15865  dvmptid  15866  dvmptc  15867  dvmptfsum  15875  dveflem  15876  plymullem1  15898  sinhalfpilem  15942  efhalfpi  15950  cospi  15951  efipi  15952  sin2pi  15954  cos2pi  15955  ef2pi  15956  sin2pim  15964  cos2pim  15965  sinmpi  15966  cosmpi  15967  sinppi  15968  cosppi  15969  sincosq4sgn  15980  tangtx  15989  sincos4thpi  15991  sincos6thpi  15993  sincos3rdpi  15994  abssinper  15997  cosq34lt1  16001  logfac  16048  1cxp  16055  ecxp  16056  rpcxpsqrt  16077  rpelogb  16104  2logb9irrALT  16129  zprmlogbaplem2  16135  binom4  16138  log2tlbndlog2  16139  log2ublem1  16140  log2ublem2  16141  log2ublem3  16142  log2ublog2  16143  birthdaylog2  16147  1sgmprm  16189  ppiublem2  16193  ppiqub  16194  bcp1ctr  16204  bclbnd  16205  bposlem4  16212  lgslem1  16217  lgsdir2lem1  16245  lgsdir2lem2  16246  lgsdir2lem3  16247  lgsdir2lem5  16249  lgs1  16261  gausslemma2dlem1a  16275  gausslemma2dlem3  16280  gausslemma2dlem4  16281  gausslemma2d  16286  lgseisenlem1  16287  lgseisenlem3  16289  lgsquadlem1  16294  lgsquadlem2  16295  lgsquad2lem2  16299  m1lgs  16302  2lgslem1a2  16304  2sqlem8  16340  setsiedg  16391  vdegp1cid  16655  clwwlknonex2lem1  16776  ex-exp  16839  ex-bc  16841  ex-gcd  16843  cvgcmp2nlemabs  17179