Theorem oveq2i 6024

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 6021	. 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 6013

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 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-iota 5284  df-fv 5332  df-ov 6016

This theorem is referenced by:  caov32  6205  oa1suc  6630  nnm1  6688  nnm2  6689  mapsnconst  6858  mapsncnv  6859  exmidpw2en  7097  mulidnq  7599  halfnqq  7620  addpinq1  7674  addnqpr1  7772  caucvgprlemm  7878  caucvgprprlemval  7898  caucvgprprlemnbj  7903  caucvgprprlemmu  7905  caucvgprprlemaddq  7918  caucvgprprlem1  7919  caucvgprprlem2  7920  m1p1sr  7970  m1m1sr  7971  0idsr  7977  1idsr  7978  00sr  7979  pn0sr  7981  ltm1sr  7987  caucvgsrlemoffres  8010  caucvgsr  8012  mulresr  8048  pitonnlem2  8057  axi2m1  8085  ax1rid  8087  axcnre  8091  add42i  8335  negid  8416  negsub  8417  subneg  8418  negsubdii  8454  apreap  8757  recexaplem2  8822  muleqadd  8838  crap0  9128  2p2e4  9260  3p2e5  9275  3p3e6  9276  4p2e6  9277  4p3e7  9278  4p4e8  9279  5p2e7  9280  5p3e8  9281  5p4e9  9282  6p2e8  9283  6p3e9  9284  7p2e9  9285  3t3e9  9291  8th4div3  9353  halfpm6th  9354  iap0  9357  addltmul  9371  div4p1lem1div2  9388  peano2z  9505  nn0n0n1ge2  9540  nneoor  9572  zeo  9575  numsuc  9614  numltc  9626  numsucc  9640  numma  9644  nummul1c  9649  decrmac  9658  decsubi  9663  decmul1  9664  decmul10add  9669  6p5lem  9670  5p5e10  9671  6p4e10  9672  7p3e10  9675  8p2e10  9680  4t3lem  9697  9t11e99  9730  decbin2  9741  fztp  10303  fzprval  10307  fztpval  10308  fzshftral  10333  fz0tp  10347  fz0to3un2pr  10348  fzo01  10451  fzo12sn  10452  fzo0to2pr  10453  fzo0to3tp  10454  fzo0to42pr  10455  intqfrac2  10571  intfracq  10572  xnn0nnen  10689  sqval  10849  sq4e2t8  10889  cu2  10890  i3  10893  i4  10894  binom2i  10900  binom3  10909  3dec  10966  faclbnd  10993  faclbnd2  10994  bcn1  11010  bcn2  11016  4bc3eq4  11025  4bc2eq6  11026  ccatlid  11173  ccatrid  11174  pfx1  11274  pfxccatin12lem3  11303  pfxccatpfx1  11307  pfxccatpfx2  11308  cats1fvn  11335  cats1catd  11339  cats2catd  11340  reim0  11412  cji  11453  resqrexlemover  11561  resqrexlemcalc1  11565  resqrexlemcalc3  11567  absi  11610  fsump1i  11984  fsumconst  12005  modfsummodlemstep  12008  arisum2  12050  geoihalfsum  12073  mertenslemi1  12086  mertenslem2  12087  mertensabs  12088  fprodconst  12171  fprodrec  12180  ef0lem  12211  ege2le3  12222  eft0val  12244  ef4p  12245  efgt1p2  12246  efgt1p  12247  tanval2ap  12264  efival  12283  ef01bndlem  12307  sin01bnd  12308  cos01bnd  12309  cos1bnd  12310  cos2bnd  12311  3dvdsdec  12416  3dvds2dec  12417  odd2np1lem  12423  odd2np1  12424  oddp1even  12427  mod2eq1n2dvds  12430  opoe  12446  bits0  12499  0bits  12510  6gcd4e2  12556  lcmneg  12636  3lcm2e6woprm  12648  6lcm4e12  12649  3prm  12690  3lcm2e6  12722  sqrt2irrlem  12723  pw2dvdslemn  12727  phiprm  12785  prmdiv  12797  pythagtriplem12  12838  pythagtriplem14  12840  pcfac  12913  prmpwdvds  12918  pockthi  12921  4sqlem5  12945  4sqlem13m  12966  modxai  12979  gcdi  12983  numexpp1  12987  numexp2x  12988  decsplit0b  12989  decsplit1  12991  decsplit  12992  2exp5  12995  2exp7  12997  2exp11  12999  2exp16  13000  ressval2  13139  ecqusaddd  13815  gsumfzconstf  13919  znbas  14648  znzrh2  14650  restin  14890  uptx  14988  cnrehmeocntop  15324  hoverb  15362  dvexp  15425  dvmptidcn  15428  dvmptccn  15429  dvmptid  15430  dvmptc  15431  dvmptfsum  15439  dveflem  15440  plymullem1  15462  sinhalfpilem  15505  efhalfpi  15513  cospi  15514  efipi  15515  sin2pi  15517  cos2pi  15518  ef2pi  15519  sin2pim  15527  cos2pim  15528  sinmpi  15529  cosmpi  15530  sinppi  15531  cosppi  15532  sincosq4sgn  15543  tangtx  15552  sincos4thpi  15554  sincos6thpi  15556  sincos3rdpi  15557  abssinper  15560  cosq34lt1  15564  1cxp  15614  ecxp  15615  rpcxpsqrt  15636  rpelogb  15663  2logb9irrALT  15688  binom4  15693  1sgmprm  15708  lgslem1  15719  lgsdir2lem1  15747  lgsdir2lem2  15748  lgsdir2lem3  15749  lgsdir2lem5  15751  lgs1  15763  gausslemma2dlem1a  15777  gausslemma2dlem3  15782  gausslemma2dlem4  15783  gausslemma2d  15788  lgseisenlem1  15789  lgseisenlem3  15791  lgsquadlem1  15796  lgsquadlem2  15797  lgsquad2lem2  15801  m1lgs  15804  2lgslem1a2  15806  2sqlem8  15842  setsiedg  15893  clwwlknonex2lem1  16232  ex-exp  16259  ex-bc  16261  ex-gcd  16263  cvgcmp2nlemabs  16572