Theorem oveq2i 6012

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 6009	. 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 1395  (class class class)co 6001

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326  df-ov 6004

This theorem is referenced by:  caov32  6193  oa1suc  6613  nnm1  6671  nnm2  6672  mapsnconst  6841  mapsncnv  6842  exmidpw2en  7074  mulidnq  7576  halfnqq  7597  addpinq1  7651  addnqpr1  7749  caucvgprlemm  7855  caucvgprprlemval  7875  caucvgprprlemnbj  7880  caucvgprprlemmu  7882  caucvgprprlemaddq  7895  caucvgprprlem1  7896  caucvgprprlem2  7897  m1p1sr  7947  m1m1sr  7948  0idsr  7954  1idsr  7955  00sr  7956  pn0sr  7958  ltm1sr  7964  caucvgsrlemoffres  7987  caucvgsr  7989  mulresr  8025  pitonnlem2  8034  axi2m1  8062  ax1rid  8064  axcnre  8068  add42i  8312  negid  8393  negsub  8394  subneg  8395  negsubdii  8431  apreap  8734  recexaplem2  8799  muleqadd  8815  crap0  9105  2p2e4  9237  3p2e5  9252  3p3e6  9253  4p2e6  9254  4p3e7  9255  4p4e8  9256  5p2e7  9257  5p3e8  9258  5p4e9  9259  6p2e8  9260  6p3e9  9261  7p2e9  9262  3t3e9  9268  8th4div3  9330  halfpm6th  9331  iap0  9334  addltmul  9348  div4p1lem1div2  9365  peano2z  9482  nn0n0n1ge2  9517  nneoor  9549  zeo  9552  numsuc  9591  numltc  9603  numsucc  9617  numma  9621  nummul1c  9626  decrmac  9635  decsubi  9640  decmul1  9641  decmul10add  9646  6p5lem  9647  5p5e10  9648  6p4e10  9649  7p3e10  9652  8p2e10  9657  4t3lem  9674  9t11e99  9707  decbin2  9718  fztp  10274  fzprval  10278  fztpval  10279  fzshftral  10304  fz0tp  10318  fz0to3un2pr  10319  fzo01  10422  fzo12sn  10423  fzo0to2pr  10424  fzo0to3tp  10425  fzo0to42pr  10426  intqfrac2  10541  intfracq  10542  xnn0nnen  10659  sqval  10819  sq4e2t8  10859  cu2  10860  i3  10863  i4  10864  binom2i  10870  binom3  10879  3dec  10936  faclbnd  10963  faclbnd2  10964  bcn1  10980  bcn2  10986  4bc3eq4  10995  4bc2eq6  10996  ccatlid  11141  ccatrid  11142  pfx1  11235  pfxccatin12lem3  11264  pfxccatpfx1  11268  pfxccatpfx2  11269  cats1fvn  11296  cats1catd  11300  cats2catd  11301  reim0  11372  cji  11413  resqrexlemover  11521  resqrexlemcalc1  11525  resqrexlemcalc3  11527  absi  11570  fsump1i  11944  fsumconst  11965  modfsummodlemstep  11968  arisum2  12010  geoihalfsum  12033  mertenslemi1  12046  mertenslem2  12047  mertensabs  12048  fprodconst  12131  fprodrec  12140  ef0lem  12171  ege2le3  12182  eft0val  12204  ef4p  12205  efgt1p2  12206  efgt1p  12207  tanval2ap  12224  efival  12243  ef01bndlem  12267  sin01bnd  12268  cos01bnd  12269  cos1bnd  12270  cos2bnd  12271  3dvdsdec  12376  3dvds2dec  12377  odd2np1lem  12383  odd2np1  12384  oddp1even  12387  mod2eq1n2dvds  12390  opoe  12406  bits0  12459  0bits  12470  6gcd4e2  12516  lcmneg  12596  3lcm2e6woprm  12608  6lcm4e12  12609  3prm  12650  3lcm2e6  12682  sqrt2irrlem  12683  pw2dvdslemn  12687  phiprm  12745  prmdiv  12757  pythagtriplem12  12798  pythagtriplem14  12800  pcfac  12873  prmpwdvds  12878  pockthi  12881  4sqlem5  12905  4sqlem13m  12926  modxai  12939  gcdi  12943  numexpp1  12947  numexp2x  12948  decsplit0b  12949  decsplit1  12951  decsplit  12952  2exp5  12955  2exp7  12957  2exp11  12959  2exp16  12960  ressval2  13099  ecqusaddd  13775  gsumfzconstf  13879  znbas  14608  znzrh2  14610  restin  14850  uptx  14948  cnrehmeocntop  15284  hoverb  15322  dvexp  15385  dvmptidcn  15388  dvmptccn  15389  dvmptid  15390  dvmptc  15391  dvmptfsum  15399  dveflem  15400  plymullem1  15422  sinhalfpilem  15465  efhalfpi  15473  cospi  15474  efipi  15475  sin2pi  15477  cos2pi  15478  ef2pi  15479  sin2pim  15487  cos2pim  15488  sinmpi  15489  cosmpi  15490  sinppi  15491  cosppi  15492  sincosq4sgn  15503  tangtx  15512  sincos4thpi  15514  sincos6thpi  15516  sincos3rdpi  15517  abssinper  15520  cosq34lt1  15524  1cxp  15574  ecxp  15575  rpcxpsqrt  15596  rpelogb  15623  2logb9irrALT  15648  binom4  15653  1sgmprm  15668  lgslem1  15679  lgsdir2lem1  15707  lgsdir2lem2  15708  lgsdir2lem3  15709  lgsdir2lem5  15711  lgs1  15723  gausslemma2dlem1a  15737  gausslemma2dlem3  15742  gausslemma2dlem4  15743  gausslemma2d  15748  lgseisenlem1  15749  lgseisenlem3  15751  lgsquadlem1  15756  lgsquadlem2  15757  lgsquad2lem2  15761  m1lgs  15764  2lgslem1a2  15766  2sqlem8  15802  setsiedg  15853  ex-exp  16091  ex-bc  16093  ex-gcd  16095  cvgcmp2nlemabs  16400