Theorem oveq2i 6096

Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)

Hypothesis

Ref	Expression
oveq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
oveq2i	⊢ (𝐶𝐹𝐴) = (𝐶𝐹𝐵)

Proof of Theorem oveq2i

Step	Hyp	Ref	Expression
1		oveq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		oveq2 6093	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶𝐹𝐴) = (𝐶𝐹𝐵)

This proof depends on syntax axioms:   = wceq 1402  (class class class)co 6085

This proof depends on 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 proof 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 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385  df-ov 6088

This theorem is used by:  caov32  6277  oa1suc  6740  nnm1  6798  nnm2  6799  mapsnconst  6976  mapsncnv  6977  exmidpw2en  7219  mulidnq  7757  halfnqq  7778  addpinq1  7832  addnqpr1  7930  caucvgprlemm  8036  caucvgprprlemval  8056  caucvgprprlemnbj  8061  caucvgprprlemmu  8063  caucvgprprlemaddq  8076  caucvgprprlem1  8077  caucvgprprlem2  8078  m1p1sr  8128  m1m1sr  8129  0idsr  8135  1idsr  8136  00sr  8137  pn0sr  8139  ltm1sr  8145  caucvgsrlemoffres  8168  caucvgsr  8170  mulresr  8206  pitonnlem2  8215  axi2m1  8243  ax1rid  8245  axcnre  8249  add42i  8494  negid  8575  negsub  8576  subneg  8577  negsubdii  8613  apreap  8918  recexaplem2  8983  muleqadd  9001  crap0  9291  2p2e4  9434  3p2e5  9449  3p3e6  9450  4p2e6  9451  4p3e7  9452  4p4e8  9453  5p2e7  9454  5p3e8  9455  5p4e9  9456  6p2e8  9457  6p3e9  9458  7p2e9  9459  3t3e9  9466  8th4div3  9529  halfpm6th  9530  iap0  9533  addltmul  9547  div4p1lem1div2  9564  peano2z  9685  nn0n0n1ge2  9720  nneoor  9753  zeo  9756  numsuc  9795  numltc  9812  numsucc  9826  numma  9830  nummul1c  9835  decrmac  9844  decsubi  9849  decmul1  9850  decmul10add  9855  6p5lem  9856  5p5e10  9857  6p4e10  9858  7p3e10  9861  8p2e10  9866  4t3lem  9883  9t11e99  9916  decbin2  9927  fz00m1  10462  fztp  10496  fzprval  10500  fztpval  10501  fzshftral  10526  fz0tp  10540  fz0to3un2pr  10541  fzo01  10645  fzo12sn  10646  fzo0to2pr  10647  fzo0to3tp  10648  fzo0to42pr  10649  intqfrac2  10771  intfracq  10772  xnn0nnen  10889  sqval  11049  sq4e2t8  11089  cu2  11090  i3  11093  i4  11094  binom2i  11100  binom3  11109  3dec  11168  faclbnd  11195  faclbnd2  11196  bcn1  11212  bcn2  11218  4bc3eq4  11228  4bc2eq6  11229  hashmap  11284  hashfibclem  11298  ccatlid  11390  ccatrid  11391  pfx1  11491  pfxccatin12lem3  11520  pfxccatpfx1  11524  pfxccatpfx2  11525  cats1fvn  11552  cats1catd  11556  cats2catd  11557  reim0  11642  cji  11684  resqrexlemover  11792  resqrexlemcalc1  11796  resqrexlemcalc3  11798  absi  11841  fsump1i  12219  fsumconst  12240  modfsummodlemstep  12243  arisum2  12285  geoihalfsum  12308  mertenslemi1  12321  mertenslem2  12322  mertensabs  12323  fprodconst  12406  fprodrec  12415  ef0lem  12446  ege2le3  12457  eft0val  12479  ef4p  12480  efgt1p2  12481  efgt1p  12482  tanval2ap  12499  efival  12518  ef01bndlem  12542  sin01bnd  12543  cos01bnd  12544  cos1bnd  12545  cos2bnd  12546  3dvdsdec  12651  3dvds2dec  12652  odd2np1lem  12658  odd2np1  12659  oddp1even  12662  mod2eq1n2dvds  12665  opoe  12681  bits0  12734  0bits  12745  6gcd4e2  12791  lcmneg  12871  3lcm2e6woprm  12883  6lcm4e12  12884  3prm  12925  3lcm2e6  12958  sqrt2irrlem  12959  pwbdvdslemn  12963  phiprm  13024  prmdiv  13036  pythagtriplem12  13077  pythagtriplem14  13079  pcfac  13152  prmpwdvds  13157  pockthi  13160  4sqlem5  13184  4sqlem13m  13205  modxai  13218  mod2xnegi  13221  gcdi  13223  numexpp1  13227  numexp2x  13228  decsplit0b  13229  decsplit1  13231  decsplit  13232  2exp5  13235  2exp7  13237  2exp11  13239  2exp16  13240  prmlem0  13243  139prm  13261  163prm  13262  317prm  13263  631prm  13264  1259lem4  13268  1259lem5  13269  1259prm  13270  ballotfilem2  13280  ballotfilemth  13333  ressval2  13473  ecqusaddd  14094  gzsumconstf  14228  gsumzfi  14242  gsumclfi  14243  gsummptfidmadd  14245  gsumsubmclfi  14247  gsummhmfi  14248  gsumconstcmn  14250  gsumfsum  15007  znbas  15063  znzrh2  15065  restin  15368  uptx  15466  cnrehmeocntop  15802  hoverb  15840  dvexp  15903  dvmptidcn  15906  dvmptccn  15907  dvmptid  15908  dvmptc  15909  dvmptfsum  15917  dveflem  15918  plymullem1  15940  sinhalfpilem  15984  efhalfpi  15992  cospi  15993  efipi  15994  sin2pi  15996  cos2pi  15997  ef2pi  15998  sin2pim  16006  cos2pim  16007  sinmpi  16008  cosmpi  16009  sinppi  16010  cosppi  16011  sincosq4sgn  16022  tangtx  16031  sincos4thpi  16033  sincos6thpi  16035  sincos3rdpi  16036  abssinper  16039  cosq34lt1  16043  logfac  16090  1cxp  16097  ecxp  16098  rpcxpsqrt  16119  rpelogb  16146  2logb9irrALT  16171  zprmlogbaplem2  16177  binom4  16180  log2tlbndlog2  16181  log2ublem1  16182  log2ublem2  16183  log2ublem3  16184  log2ublog2  16185  birthdaylog2  16189  cht1  16232  1sgmprm  16249  ppiublem2  16253  ppiqub  16254  chtublem  16256  chtqub  16257  bcp1ctr  16267  bclbnd  16268  bposlem4  16275  bposlem6  16277  bposlem8  16279  bposlem9  16280  lgslem1  16285  lgsdir2lem1  16313  lgsdir2lem2  16314  lgsdir2lem3  16315  lgsdir2lem5  16317  lgs1  16329  gausslemma2dlem1a  16343  gausslemma2dlem3  16348  gausslemma2dlem4  16349  gausslemma2d  16354  lgseisenlem1  16355  lgseisenlem3  16357  lgsquadlem1  16362  lgsquadlem2  16363  lgsquad2lem2  16367  m1lgs  16370  2lgslem1a2  16372  2sqlem8  16408  setsiedg  16459  vdegp1cid  16723  clwwlknonex2lem1  16844  ex-exp  16907  ex-bc  16909  ex-gcd  16911  cvgcmp2nlemabs  17247