Theorem oveq2i 6063

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 6060	. 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 1398  (class class class)co 6052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-v 2817  df-un 3217  df-sn 3697  df-pr 3698  df-op 3700  df-uni 3917  df-br 4112  df-iota 5314  df-fv 5362  df-ov 6055

This theorem is referenced by:  caov32  6244  oa1suc  6702  nnm1  6760  nnm2  6761  mapsnconst  6931  mapsncnv  6932  exmidpw2en  7174  mulidnq  7706  halfnqq  7727  addpinq1  7781  addnqpr1  7879  caucvgprlemm  7985  caucvgprprlemval  8005  caucvgprprlemnbj  8010  caucvgprprlemmu  8012  caucvgprprlemaddq  8025  caucvgprprlem1  8026  caucvgprprlem2  8027  m1p1sr  8077  m1m1sr  8078  0idsr  8084  1idsr  8085  00sr  8086  pn0sr  8088  ltm1sr  8094  caucvgsrlemoffres  8117  caucvgsr  8119  mulresr  8155  pitonnlem2  8164  axi2m1  8192  ax1rid  8194  axcnre  8198  add42i  8441  negid  8522  negsub  8523  subneg  8524  negsubdii  8560  apreap  8863  recexaplem2  8928  muleqadd  8944  crap0  9234  2p2e4  9366  3p2e5  9381  3p3e6  9382  4p2e6  9383  4p3e7  9384  4p4e8  9385  5p2e7  9386  5p3e8  9387  5p4e9  9388  6p2e8  9389  6p3e9  9390  7p2e9  9391  3t3e9  9397  8th4div3  9459  halfpm6th  9460  iap0  9463  addltmul  9477  div4p1lem1div2  9494  peano2z  9615  nn0n0n1ge2  9650  nneoor  9683  zeo  9686  numsuc  9725  numltc  9737  numsucc  9751  numma  9755  nummul1c  9760  decrmac  9769  decsubi  9774  decmul1  9775  decmul10add  9780  6p5lem  9781  5p5e10  9782  6p4e10  9783  7p3e10  9786  8p2e10  9791  4t3lem  9808  9t11e99  9841  decbin2  9852  fztp  10416  fzprval  10420  fztpval  10421  fzshftral  10446  fz0tp  10460  fz0to3un2pr  10461  fzo01  10565  fzo12sn  10566  fzo0to2pr  10567  fzo0to3tp  10568  fzo0to42pr  10569  intqfrac2  10685  intfracq  10686  xnn0nnen  10803  sqval  10963  sq4e2t8  11003  cu2  11004  i3  11007  i4  11008  binom2i  11014  binom3  11023  3dec  11080  faclbnd  11107  faclbnd2  11108  bcn1  11124  bcn2  11130  4bc3eq4  11140  4bc2eq6  11141  hashmap  11196  hashfibclem  11210  ccatlid  11298  ccatrid  11299  pfx1  11399  pfxccatin12lem3  11428  pfxccatpfx1  11432  pfxccatpfx2  11433  cats1fvn  11460  cats1catd  11464  cats2catd  11465  reim0  11550  cji  11591  resqrexlemover  11699  resqrexlemcalc1  11703  resqrexlemcalc3  11705  absi  11748  fsump1i  12123  fsumconst  12144  modfsummodlemstep  12147  arisum2  12189  geoihalfsum  12212  mertenslemi1  12225  mertenslem2  12226  mertensabs  12227  fprodconst  12310  fprodrec  12319  ef0lem  12350  ege2le3  12361  eft0val  12383  ef4p  12384  efgt1p2  12385  efgt1p  12386  tanval2ap  12403  efival  12422  ef01bndlem  12446  sin01bnd  12447  cos01bnd  12448  cos1bnd  12449  cos2bnd  12450  3dvdsdec  12555  3dvds2dec  12556  odd2np1lem  12562  odd2np1  12563  oddp1even  12566  mod2eq1n2dvds  12569  opoe  12585  bits0  12638  0bits  12649  6gcd4e2  12695  lcmneg  12775  3lcm2e6woprm  12787  6lcm4e12  12788  3prm  12829  3lcm2e6  12861  sqrt2irrlem  12862  pw2dvdslemn  12866  phiprm  12924  prmdiv  12936  pythagtriplem12  12977  pythagtriplem14  12979  pcfac  13052  prmpwdvds  13057  pockthi  13060  4sqlem5  13084  4sqlem13m  13105  modxai  13118  gcdi  13122  numexpp1  13126  numexp2x  13127  decsplit0b  13128  decsplit1  13130  decsplit  13131  2exp5  13134  2exp7  13136  2exp11  13138  2exp16  13139  ballotfilem2  13149  ressval2  13296  ecqusaddd  13972  gsumfzconstf  14076  znbas  14809  znzrh2  14811  restin  15058  uptx  15156  cnrehmeocntop  15492  hoverb  15530  dvexp  15593  dvmptidcn  15596  dvmptccn  15597  dvmptid  15598  dvmptc  15599  dvmptfsum  15607  dveflem  15608  plymullem1  15630  sinhalfpilem  15673  efhalfpi  15681  cospi  15682  efipi  15683  sin2pi  15685  cos2pi  15686  ef2pi  15687  sin2pim  15695  cos2pim  15696  sinmpi  15697  cosmpi  15698  sinppi  15699  cosppi  15700  sincosq4sgn  15711  tangtx  15720  sincos4thpi  15722  sincos6thpi  15724  sincos3rdpi  15725  abssinper  15728  cosq34lt1  15732  1cxp  15782  ecxp  15783  rpcxpsqrt  15804  rpelogb  15831  2logb9irrALT  15856  binom4  15861  1sgmprm  15879  lgslem1  15890  lgsdir2lem1  15918  lgsdir2lem2  15919  lgsdir2lem3  15920  lgsdir2lem5  15922  lgs1  15934  gausslemma2dlem1a  15948  gausslemma2dlem3  15953  gausslemma2dlem4  15954  gausslemma2d  15959  lgseisenlem1  15960  lgseisenlem3  15962  lgsquadlem1  15967  lgsquadlem2  15968  lgsquad2lem2  15972  m1lgs  15975  2lgslem1a2  15977  2sqlem8  16013  setsiedg  16064  vdegp1cid  16328  clwwlknonex2lem1  16449  ex-exp  16512  ex-bc  16514  ex-gcd  16516  cvgcmp2nlemabs  16833  gfsumz  16886  gfsumcl  16887