Theorem oveq2i 6039

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 6036	. 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 6028

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 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rex 2517  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-iota 5293  df-fv 5341  df-ov 6031

This theorem is referenced by:  caov32  6220  oa1suc  6678  nnm1  6736  nnm2  6737  mapsnconst  6906  mapsncnv  6907  exmidpw2en  7147  mulidnq  7669  halfnqq  7690  addpinq1  7744  addnqpr1  7842  caucvgprlemm  7948  caucvgprprlemval  7968  caucvgprprlemnbj  7973  caucvgprprlemmu  7975  caucvgprprlemaddq  7988  caucvgprprlem1  7989  caucvgprprlem2  7990  m1p1sr  8040  m1m1sr  8041  0idsr  8047  1idsr  8048  00sr  8049  pn0sr  8051  ltm1sr  8057  caucvgsrlemoffres  8080  caucvgsr  8082  mulresr  8118  pitonnlem2  8127  axi2m1  8155  ax1rid  8157  axcnre  8161  add42i  8404  negid  8485  negsub  8486  subneg  8487  negsubdii  8523  apreap  8826  recexaplem2  8891  muleqadd  8907  crap0  9197  2p2e4  9329  3p2e5  9344  3p3e6  9345  4p2e6  9346  4p3e7  9347  4p4e8  9348  5p2e7  9349  5p3e8  9350  5p4e9  9351  6p2e8  9352  6p3e9  9353  7p2e9  9354  3t3e9  9360  8th4div3  9422  halfpm6th  9423  iap0  9426  addltmul  9440  div4p1lem1div2  9457  peano2z  9576  nn0n0n1ge2  9611  nneoor  9643  zeo  9646  numsuc  9685  numltc  9697  numsucc  9711  numma  9715  nummul1c  9720  decrmac  9729  decsubi  9734  decmul1  9735  decmul10add  9740  6p5lem  9741  5p5e10  9742  6p4e10  9743  7p3e10  9746  8p2e10  9751  4t3lem  9768  9t11e99  9801  decbin2  9812  fztp  10375  fzprval  10379  fztpval  10380  fzshftral  10405  fz0tp  10419  fz0to3un2pr  10420  fzo01  10524  fzo12sn  10525  fzo0to2pr  10526  fzo0to3tp  10527  fzo0to42pr  10528  intqfrac2  10644  intfracq  10645  xnn0nnen  10762  sqval  10922  sq4e2t8  10962  cu2  10963  i3  10966  i4  10967  binom2i  10973  binom3  10982  3dec  11039  faclbnd  11066  faclbnd2  11067  bcn1  11083  bcn2  11089  4bc3eq4  11098  4bc2eq6  11099  ccatlid  11249  ccatrid  11250  pfx1  11350  pfxccatin12lem3  11379  pfxccatpfx1  11383  pfxccatpfx2  11384  cats1fvn  11411  cats1catd  11415  cats2catd  11416  reim0  11501  cji  11542  resqrexlemover  11650  resqrexlemcalc1  11654  resqrexlemcalc3  11656  absi  11699  fsump1i  12074  fsumconst  12095  modfsummodlemstep  12098  arisum2  12140  geoihalfsum  12163  mertenslemi1  12176  mertenslem2  12177  mertensabs  12178  fprodconst  12261  fprodrec  12270  ef0lem  12301  ege2le3  12312  eft0val  12334  ef4p  12335  efgt1p2  12336  efgt1p  12337  tanval2ap  12354  efival  12373  ef01bndlem  12397  sin01bnd  12398  cos01bnd  12399  cos1bnd  12400  cos2bnd  12401  3dvdsdec  12506  3dvds2dec  12507  odd2np1lem  12513  odd2np1  12514  oddp1even  12517  mod2eq1n2dvds  12520  opoe  12536  bits0  12589  0bits  12600  6gcd4e2  12646  lcmneg  12726  3lcm2e6woprm  12738  6lcm4e12  12739  3prm  12780  3lcm2e6  12812  sqrt2irrlem  12813  pw2dvdslemn  12817  phiprm  12875  prmdiv  12887  pythagtriplem12  12928  pythagtriplem14  12930  pcfac  13003  prmpwdvds  13008  pockthi  13011  4sqlem5  13035  4sqlem13m  13056  modxai  13069  gcdi  13073  numexpp1  13077  numexp2x  13078  decsplit0b  13079  decsplit1  13081  decsplit  13082  2exp5  13085  2exp7  13087  2exp11  13089  2exp16  13090  ressval2  13229  ecqusaddd  13905  gsumfzconstf  14009  znbas  14740  znzrh2  14742  restin  14987  uptx  15085  cnrehmeocntop  15421  hoverb  15459  dvexp  15522  dvmptidcn  15525  dvmptccn  15526  dvmptid  15527  dvmptc  15528  dvmptfsum  15536  dveflem  15537  plymullem1  15559  sinhalfpilem  15602  efhalfpi  15610  cospi  15611  efipi  15612  sin2pi  15614  cos2pi  15615  ef2pi  15616  sin2pim  15624  cos2pim  15625  sinmpi  15626  cosmpi  15627  sinppi  15628  cosppi  15629  sincosq4sgn  15640  tangtx  15649  sincos4thpi  15651  sincos6thpi  15653  sincos3rdpi  15654  abssinper  15657  cosq34lt1  15661  1cxp  15711  ecxp  15712  rpcxpsqrt  15733  rpelogb  15760  2logb9irrALT  15785  binom4  15790  1sgmprm  15808  lgslem1  15819  lgsdir2lem1  15847  lgsdir2lem2  15848  lgsdir2lem3  15849  lgsdir2lem5  15851  lgs1  15863  gausslemma2dlem1a  15877  gausslemma2dlem3  15882  gausslemma2dlem4  15883  gausslemma2d  15888  lgseisenlem1  15889  lgseisenlem3  15891  lgsquadlem1  15896  lgsquadlem2  15897  lgsquad2lem2  15901  m1lgs  15904  2lgslem1a2  15906  2sqlem8  15942  setsiedg  15993  vdegp1cid  16257  clwwlknonex2lem1  16378  ex-exp  16441  ex-bc  16443  ex-gcd  16445  cvgcmp2nlemabs  16764  gfsumcl  16816