Theorem oveq2i 6089

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 6086	. 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 1402  (class class class)co 6078

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 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 theorem 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 3714  df-pr 3715  df-op 3717  df-uni 3934  df-br 4129  df-iota 5335  df-fv 5383  df-ov 6081

This theorem is referenced by:  caov32  6270  oa1suc  6733  nnm1  6791  nnm2  6792  mapsnconst  6969  mapsncnv  6970  exmidpw2en  7212  mulidnq  7749  halfnqq  7770  addpinq1  7824  addnqpr1  7922  caucvgprlemm  8028  caucvgprprlemval  8048  caucvgprprlemnbj  8053  caucvgprprlemmu  8055  caucvgprprlemaddq  8068  caucvgprprlem1  8069  caucvgprprlem2  8070  m1p1sr  8120  m1m1sr  8121  0idsr  8127  1idsr  8128  00sr  8129  pn0sr  8131  ltm1sr  8137  caucvgsrlemoffres  8160  caucvgsr  8162  mulresr  8198  pitonnlem2  8207  axi2m1  8235  ax1rid  8237  axcnre  8241  add42i  8485  negid  8566  negsub  8567  subneg  8568  negsubdii  8604  apreap  8908  recexaplem2  8973  muleqadd  8991  crap0  9281  2p2e4  9413  3p2e5  9428  3p3e6  9429  4p2e6  9430  4p3e7  9431  4p4e8  9432  5p2e7  9433  5p3e8  9434  5p4e9  9435  6p2e8  9436  6p3e9  9437  7p2e9  9438  3t3e9  9444  8th4div3  9506  halfpm6th  9507  iap0  9510  addltmul  9524  div4p1lem1div2  9541  peano2z  9662  nn0n0n1ge2  9697  nneoor  9730  zeo  9733  numsuc  9772  numltc  9784  numsucc  9798  numma  9802  nummul1c  9807  decrmac  9816  decsubi  9821  decmul1  9822  decmul10add  9827  6p5lem  9828  5p5e10  9829  6p4e10  9830  7p3e10  9833  8p2e10  9838  4t3lem  9855  9t11e99  9888  decbin2  9899  fztp  10466  fzprval  10470  fztpval  10471  fzshftral  10496  fz0tp  10510  fz0to3un2pr  10511  fzo01  10615  fzo12sn  10616  fzo0to2pr  10617  fzo0to3tp  10618  fzo0to42pr  10619  intqfrac2  10737  intfracq  10738  xnn0nnen  10855  sqval  11015  sq4e2t8  11055  cu2  11056  i3  11059  i4  11060  binom2i  11066  binom3  11075  3dec  11133  faclbnd  11160  faclbnd2  11161  bcn1  11177  bcn2  11183  4bc3eq4  11193  4bc2eq6  11194  hashmap  11249  hashfibclem  11263  ccatlid  11355  ccatrid  11356  pfx1  11456  pfxccatin12lem3  11485  pfxccatpfx1  11489  pfxccatpfx2  11490  cats1fvn  11517  cats1catd  11521  cats2catd  11522  reim0  11607  cji  11649  resqrexlemover  11757  resqrexlemcalc1  11761  resqrexlemcalc3  11763  absi  11806  fsump1i  12181  fsumconst  12202  modfsummodlemstep  12205  arisum2  12247  geoihalfsum  12270  mertenslemi1  12283  mertenslem2  12284  mertensabs  12285  fprodconst  12368  fprodrec  12377  ef0lem  12408  ege2le3  12419  eft0val  12441  ef4p  12442  efgt1p2  12443  efgt1p  12444  tanval2ap  12461  efival  12480  ef01bndlem  12504  sin01bnd  12505  cos01bnd  12506  cos1bnd  12507  cos2bnd  12508  3dvdsdec  12613  3dvds2dec  12614  odd2np1lem  12620  odd2np1  12621  oddp1even  12624  mod2eq1n2dvds  12627  opoe  12643  bits0  12696  0bits  12707  6gcd4e2  12753  lcmneg  12833  3lcm2e6woprm  12845  6lcm4e12  12846  3prm  12887  3lcm2e6  12919  sqrt2irrlem  12920  pw2dvdslemn  12924  phiprm  12982  prmdiv  12994  pythagtriplem12  13035  pythagtriplem14  13037  pcfac  13110  prmpwdvds  13115  pockthi  13118  4sqlem5  13142  4sqlem13m  13163  modxai  13176  gcdi  13180  numexpp1  13184  numexp2x  13185  decsplit0b  13186  decsplit1  13188  decsplit  13189  2exp5  13192  2exp7  13194  2exp11  13196  2exp16  13197  ballotfilem2  13209  ballotfilemth  13262  ressval2  13400  ecqusaddd  14021  gzsumconstf  14124  gsumzfi  14138  gsumclfi  14139  gsummptfidmadd  14141  gsumsubmclfi  14143  gsummhmfi  14144  gsumconstcmn  14146  gsumfsum  14898  znbas  14954  znzrh2  14956  restin  15203  uptx  15301  cnrehmeocntop  15637  hoverb  15675  dvexp  15738  dvmptidcn  15741  dvmptccn  15742  dvmptid  15743  dvmptc  15744  dvmptfsum  15752  dveflem  15753  plymullem1  15775  sinhalfpilem  15818  efhalfpi  15826  cospi  15827  efipi  15828  sin2pi  15830  cos2pi  15831  ef2pi  15832  sin2pim  15840  cos2pim  15841  sinmpi  15842  cosmpi  15843  sinppi  15844  cosppi  15845  sincosq4sgn  15856  tangtx  15865  sincos4thpi  15867  sincos6thpi  15869  sincos3rdpi  15870  abssinper  15873  cosq34lt1  15877  logfac  15921  1cxp  15928  ecxp  15929  rpcxpsqrt  15950  rpelogb  15977  2logb9irrALT  16002  binom4  16007  1sgmprm  16025  lgslem1  16036  lgsdir2lem1  16064  lgsdir2lem2  16065  lgsdir2lem3  16066  lgsdir2lem5  16068  lgs1  16080  gausslemma2dlem1a  16094  gausslemma2dlem3  16099  gausslemma2dlem4  16100  gausslemma2d  16105  lgseisenlem1  16106  lgseisenlem3  16108  lgsquadlem1  16113  lgsquadlem2  16114  lgsquad2lem2  16118  m1lgs  16121  2lgslem1a2  16123  2sqlem8  16159  setsiedg  16210  vdegp1cid  16474  clwwlknonex2lem1  16595  ex-exp  16658  ex-bc  16660  ex-gcd  16662  cvgcmp2nlemabs  16989