Theorem oveq2i 6069

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 6066	. 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 6058

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 3218  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-iota 5317  df-fv 5365  df-ov 6061

This theorem is referenced by:  caov32  6250  oa1suc  6713  nnm1  6771  nnm2  6772  mapsnconst  6942  mapsncnv  6943  exmidpw2en  7185  mulidnq  7720  halfnqq  7741  addpinq1  7795  addnqpr1  7893  caucvgprlemm  7999  caucvgprprlemval  8019  caucvgprprlemnbj  8024  caucvgprprlemmu  8026  caucvgprprlemaddq  8039  caucvgprprlem1  8040  caucvgprprlem2  8041  m1p1sr  8091  m1m1sr  8092  0idsr  8098  1idsr  8099  00sr  8100  pn0sr  8102  ltm1sr  8108  caucvgsrlemoffres  8131  caucvgsr  8133  mulresr  8169  pitonnlem2  8178  axi2m1  8206  ax1rid  8208  axcnre  8212  add42i  8455  negid  8536  negsub  8537  subneg  8538  negsubdii  8574  apreap  8878  recexaplem2  8943  muleqadd  8959  crap0  9249  2p2e4  9381  3p2e5  9396  3p3e6  9397  4p2e6  9398  4p3e7  9399  4p4e8  9400  5p2e7  9401  5p3e8  9402  5p4e9  9403  6p2e8  9404  6p3e9  9405  7p2e9  9406  3t3e9  9412  8th4div3  9474  halfpm6th  9475  iap0  9478  addltmul  9492  div4p1lem1div2  9509  peano2z  9630  nn0n0n1ge2  9665  nneoor  9698  zeo  9701  numsuc  9740  numltc  9752  numsucc  9766  numma  9770  nummul1c  9775  decrmac  9784  decsubi  9789  decmul1  9790  decmul10add  9795  6p5lem  9796  5p5e10  9797  6p4e10  9798  7p3e10  9801  8p2e10  9806  4t3lem  9823  9t11e99  9856  decbin2  9867  fztp  10434  fzprval  10438  fztpval  10439  fzshftral  10464  fz0tp  10478  fz0to3un2pr  10479  fzo01  10583  fzo12sn  10584  fzo0to2pr  10585  fzo0to3tp  10586  fzo0to42pr  10587  intqfrac2  10705  intfracq  10706  xnn0nnen  10823  sqval  10983  sq4e2t8  11023  cu2  11024  i3  11027  i4  11028  binom2i  11034  binom3  11043  3dec  11101  faclbnd  11128  faclbnd2  11129  bcn1  11145  bcn2  11151  4bc3eq4  11161  4bc2eq6  11162  hashmap  11217  hashfibclem  11231  ccatlid  11319  ccatrid  11320  pfx1  11420  pfxccatin12lem3  11449  pfxccatpfx1  11453  pfxccatpfx2  11454  cats1fvn  11481  cats1catd  11485  cats2catd  11486  reim0  11571  cji  11612  resqrexlemover  11720  resqrexlemcalc1  11724  resqrexlemcalc3  11726  absi  11769  fsump1i  12144  fsumconst  12165  modfsummodlemstep  12168  arisum2  12210  geoihalfsum  12233  mertenslemi1  12246  mertenslem2  12247  mertensabs  12248  fprodconst  12331  fprodrec  12340  ef0lem  12371  ege2le3  12382  eft0val  12404  ef4p  12405  efgt1p2  12406  efgt1p  12407  tanval2ap  12424  efival  12443  ef01bndlem  12467  sin01bnd  12468  cos01bnd  12469  cos1bnd  12470  cos2bnd  12471  3dvdsdec  12576  3dvds2dec  12577  odd2np1lem  12583  odd2np1  12584  oddp1even  12587  mod2eq1n2dvds  12590  opoe  12606  bits0  12659  0bits  12670  6gcd4e2  12716  lcmneg  12796  3lcm2e6woprm  12808  6lcm4e12  12809  3prm  12850  3lcm2e6  12882  sqrt2irrlem  12883  pw2dvdslemn  12887  phiprm  12945  prmdiv  12957  pythagtriplem12  12998  pythagtriplem14  13000  pcfac  13073  prmpwdvds  13078  pockthi  13081  4sqlem5  13105  4sqlem13m  13126  modxai  13139  gcdi  13143  numexpp1  13147  numexp2x  13148  decsplit0b  13149  decsplit1  13151  decsplit  13152  2exp5  13155  2exp7  13157  2exp11  13159  2exp16  13160  ballotfilem2  13172  ballotfilemth  13225  ressval2  13363  ecqusaddd  13991  gsumfzconstf  14095  gfsumz  14109  gfsumcl  14110  znbas  14918  znzrh2  14920  restin  15167  uptx  15265  cnrehmeocntop  15601  hoverb  15639  dvexp  15702  dvmptidcn  15705  dvmptccn  15706  dvmptid  15707  dvmptc  15708  dvmptfsum  15716  dveflem  15717  plymullem1  15739  sinhalfpilem  15782  efhalfpi  15790  cospi  15791  efipi  15792  sin2pi  15794  cos2pi  15795  ef2pi  15796  sin2pim  15804  cos2pim  15805  sinmpi  15806  cosmpi  15807  sinppi  15808  cosppi  15809  sincosq4sgn  15820  tangtx  15829  sincos4thpi  15831  sincos6thpi  15833  sincos3rdpi  15834  abssinper  15837  cosq34lt1  15841  1cxp  15891  ecxp  15892  rpcxpsqrt  15913  rpelogb  15940  2logb9irrALT  15965  binom4  15970  1sgmprm  15988  lgslem1  15999  lgsdir2lem1  16027  lgsdir2lem2  16028  lgsdir2lem3  16029  lgsdir2lem5  16031  lgs1  16043  gausslemma2dlem1a  16057  gausslemma2dlem3  16062  gausslemma2dlem4  16063  gausslemma2d  16068  lgseisenlem1  16069  lgseisenlem3  16071  lgsquadlem1  16076  lgsquadlem2  16077  lgsquad2lem2  16081  m1lgs  16084  2lgslem1a2  16086  2sqlem8  16122  setsiedg  16173  vdegp1cid  16437  clwwlknonex2lem1  16558  ex-exp  16621  ex-bc  16623  ex-gcd  16625  cvgcmp2nlemabs  16942