Theorem oveq2i 5980

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 5977	. 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 1373  (class class class)co 5969

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-rex 2492  df-v 2779  df-un 3179  df-sn 3650  df-pr 3651  df-op 3653  df-uni 3866  df-br 4061  df-iota 5252  df-fv 5299  df-ov 5972

This theorem is referenced by:  caov32  6159  oa1suc  6578  nnm1  6636  nnm2  6637  mapsnconst  6806  mapsncnv  6807  exmidpw2en  7037  mulidnq  7539  halfnqq  7560  addpinq1  7614  addnqpr1  7712  caucvgprlemm  7818  caucvgprprlemval  7838  caucvgprprlemnbj  7843  caucvgprprlemmu  7845  caucvgprprlemaddq  7858  caucvgprprlem1  7859  caucvgprprlem2  7860  m1p1sr  7910  m1m1sr  7911  0idsr  7917  1idsr  7918  00sr  7919  pn0sr  7921  ltm1sr  7927  caucvgsrlemoffres  7950  caucvgsr  7952  mulresr  7988  pitonnlem2  7997  axi2m1  8025  ax1rid  8027  axcnre  8031  add42i  8275  negid  8356  negsub  8357  subneg  8358  negsubdii  8394  apreap  8697  recexaplem2  8762  muleqadd  8778  crap0  9068  2p2e4  9200  3p2e5  9215  3p3e6  9216  4p2e6  9217  4p3e7  9218  4p4e8  9219  5p2e7  9220  5p3e8  9221  5p4e9  9222  6p2e8  9223  6p3e9  9224  7p2e9  9225  3t3e9  9231  8th4div3  9293  halfpm6th  9294  iap0  9297  addltmul  9311  div4p1lem1div2  9328  peano2z  9445  nn0n0n1ge2  9480  nneoor  9512  zeo  9515  numsuc  9554  numltc  9566  numsucc  9580  numma  9584  nummul1c  9589  decrmac  9598  decsubi  9603  decmul1  9604  decmul10add  9609  6p5lem  9610  5p5e10  9611  6p4e10  9612  7p3e10  9615  8p2e10  9620  4t3lem  9637  9t11e99  9670  decbin2  9681  fztp  10237  fzprval  10241  fztpval  10242  fzshftral  10267  fz0tp  10281  fz0to3un2pr  10282  fzo01  10384  fzo12sn  10385  fzo0to2pr  10386  fzo0to3tp  10387  fzo0to42pr  10388  intqfrac2  10503  intfracq  10504  xnn0nnen  10621  sqval  10781  sq4e2t8  10821  cu2  10822  i3  10825  i4  10826  binom2i  10832  binom3  10841  3dec  10898  faclbnd  10925  faclbnd2  10926  bcn1  10942  bcn2  10948  4bc3eq4  10957  4bc2eq6  10958  ccatlid  11102  ccatrid  11103  pfx1  11196  pfxccatin12lem3  11225  pfxccatpfx1  11229  pfxccatpfx2  11230  cats1fvn  11257  cats1catd  11261  cats2catd  11262  reim0  11333  cji  11374  resqrexlemover  11482  resqrexlemcalc1  11486  resqrexlemcalc3  11488  absi  11531  fsump1i  11905  fsumconst  11926  modfsummodlemstep  11929  arisum2  11971  geoihalfsum  11994  mertenslemi1  12007  mertenslem2  12008  mertensabs  12009  fprodconst  12092  fprodrec  12101  ef0lem  12132  ege2le3  12143  eft0val  12165  ef4p  12166  efgt1p2  12167  efgt1p  12168  tanval2ap  12185  efival  12204  ef01bndlem  12228  sin01bnd  12229  cos01bnd  12230  cos1bnd  12231  cos2bnd  12232  3dvdsdec  12337  3dvds2dec  12338  odd2np1lem  12344  odd2np1  12345  oddp1even  12348  mod2eq1n2dvds  12351  opoe  12367  bits0  12420  0bits  12431  6gcd4e2  12477  lcmneg  12557  3lcm2e6woprm  12569  6lcm4e12  12570  3prm  12611  3lcm2e6  12643  sqrt2irrlem  12644  pw2dvdslemn  12648  phiprm  12706  prmdiv  12718  pythagtriplem12  12759  pythagtriplem14  12761  pcfac  12834  prmpwdvds  12839  pockthi  12842  4sqlem5  12866  4sqlem13m  12887  modxai  12900  gcdi  12904  numexpp1  12908  numexp2x  12909  decsplit0b  12910  decsplit1  12912  decsplit  12913  2exp5  12916  2exp7  12918  2exp11  12920  2exp16  12921  ressval2  13059  ecqusaddd  13735  gsumfzconstf  13839  znbas  14567  znzrh2  14569  restin  14809  uptx  14907  cnrehmeocntop  15243  hoverb  15281  dvexp  15344  dvmptidcn  15347  dvmptccn  15348  dvmptid  15349  dvmptc  15350  dvmptfsum  15358  dveflem  15359  plymullem1  15381  sinhalfpilem  15424  efhalfpi  15432  cospi  15433  efipi  15434  sin2pi  15436  cos2pi  15437  ef2pi  15438  sin2pim  15446  cos2pim  15447  sinmpi  15448  cosmpi  15449  sinppi  15450  cosppi  15451  sincosq4sgn  15462  tangtx  15471  sincos4thpi  15473  sincos6thpi  15475  sincos3rdpi  15476  abssinper  15479  cosq34lt1  15483  1cxp  15533  ecxp  15534  rpcxpsqrt  15555  rpelogb  15582  2logb9irrALT  15607  binom4  15612  1sgmprm  15627  lgslem1  15638  lgsdir2lem1  15666  lgsdir2lem2  15667  lgsdir2lem3  15668  lgsdir2lem5  15670  lgs1  15682  gausslemma2dlem1a  15696  gausslemma2dlem3  15701  gausslemma2dlem4  15702  gausslemma2d  15707  lgseisenlem1  15708  lgseisenlem3  15710  lgsquadlem1  15715  lgsquadlem2  15716  lgsquad2lem2  15720  m1lgs  15723  2lgslem1a2  15725  2sqlem8  15761  ex-exp  15971  ex-bc  15973  ex-gcd  15975  cvgcmp2nlemabs  16281