MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oveq2i Unicode version

Theorem oveq2i 5911
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
StepHypRef Expression
1 oveq1i.1 . 2  |-  A  =  B
2 oveq2 5908 . 2  |-  ( A  =  B  ->  ( C F A )  =  ( C F B ) )
31, 2ax-mp 8 1  |-  ( C F A )  =  ( C F B )
Colors of variables: wff set class
Syntax hints:    = wceq 1633  (class class class)co 5900
This theorem is referenced by:  caov32  6089  caov4  6093  caov42  6095  seqomsuc  6511  oa1suc  6572  om1  6582  oe1  6584  oawordeulem  6594  oeoalem  6636  nnm1  6688  nnm2  6689  nneob  6692  omopthlem1  6695  mapsnconst  6856  mapsncnv  6857  map2xp  7074  cantnflt  7418  cnfcom2  7450  infxpenc  7690  infxpenc2  7694  ackbij1lem5  7895  alephom  8252  pwxpndom2  8332  adderpqlem  8623  addassnq  8627  mulcanenq  8629  distrnq  8630  ltanq  8640  ltexnq  8644  halfnq  8645  ltrnq  8648  archnq  8649  addclprlem2  8686  prlem934  8702  prlem936  8716  addcmpblnr  8739  mulcmpblnrlem  8740  ltsrpr  8744  m1p1sr  8759  m1m1sr  8760  0idsr  8764  1idsr  8765  00sr  8766  pn0sr  8768  recexsrlem  8770  mulgt0sr  8772  sqgt0sr  8773  mulresr  8806  axmulcom  8822  axmulass  8824  axdistr  8825  axi2m1  8826  ax1rid  8828  axcnre  8831  mul02lem1  9033  addid1  9037  add42i  9077  negid  9139  negsub  9140  subneg  9141  negsubdii  9176  muleqadd  9457  crne0  9784  2p2e4  9889  3p2e5  9902  3p3e6  9903  4p2e6  9904  4p3e7  9905  4p4e8  9906  5p2e7  9907  5p3e8  9908  5p4e9  9909  5p5e10  9910  6p2e8  9911  6p3e9  9912  6p4e10  9913  7p2e9  9914  7p3e10  9915  8p2e10  9916  3t3e9  9920  8th4div3  9982  halfpm6th  9983  addltmul  9994  nneo  10142  zeo  10144  numsuc  10183  numltc  10191  numsucc  10197  numma  10202  nummul1c  10207  6p5lem  10220  4t3lem  10242  decbin2  10275  xmulmnf1  10643  fztp  10888  fzprval  10891  fztpval  10892  fzshftral  10916  fzo01  10960  quoremz  11006  quoremnn0ALT  11008  intfrac2  11009  intfracq  11010  sqval  11210  sqrecii  11233  cu2  11248  i3  11251  i4  11252  binom2i  11259  binom3  11269  crreczi  11273  nn0opthlem1  11330  facp1  11340  faclbnd  11350  faclbnd2  11351  faclbnd4lem1  11353  faclbnd4lem4  11356  bcn1  11372  bcn2  11378  hashgadd  11406  hashxplem  11432  hashmap  11434  hashfun  11436  hashbclem  11437  fz1isolem  11446  ccatlid  11481  ccatrid  11482  eqs1  11494  wrdeqs1cat  11522  cats1un  11523  cats1fvn  11555  cats1cat  11558  swrds2  11607  reim0  11650  cji  11691  sqrm1  11808  absi  11818  rddif  11871  iseraltlem2  12202  iseralt  12204  fsump1i  12279  fsummulc2  12293  incexclem  12342  incexc  12343  arisum2  12366  geoihalfsum  12385  mertenslem1  12387  mertens  12389  ef0lem  12407  ege2le3  12418  eft0val  12439  ef4p  12440  efgt1p2  12441  efgt1p  12442  tanval2  12460  efival  12479  ef01bndlem  12511  sin01bnd  12512  cos01bnd  12513  cos1bnd  12514  cos2bnd  12515  rpnnen2lem11  12550  sqr2irrlem  12573  odd2np1lem  12633  odd2np1  12634  oddp1even  12636  divalglem5  12643  divalglem6  12644  bits0  12666  0bits  12677  bitsinv1lem  12679  gcdaddmlem  12754  3prm  12822  phiprm  12892  eulerthlem2  12897  prmdiv  12900  opoe  12911  pythagtriplem12  12926  pythagtriplem14  12928  pcmpt  12987  pcfac  12994  prmpwdvds  12998  pockthi  13001  prmreclem2  13011  prmreclem6  13015  4sqlem5  13036  4sqlem13  13051  modxai  13130  mod2xnegi  13133  gcdi  13135  decexp2  13137  numexpp1  13140  numexp2x  13141  decsplit0b  13142  decsplit1  13144  decsplit  13145  2exp6  13148  2exp16  13150  prmlem0  13154  139prm  13172  163prm  13173  317prm  13174  631prm  13175  1259lem1  13176  1259lem3  13178  1259lem4  13179  1259lem5  13180  1259prm  13181  2503lem1  13182  2503lem2  13183  2503lem3  13184  2503prm  13185  4001lem1  13186  4001lem2  13187  4001lem3  13188  4001lem4  13189  ressinbas  13251  rescfth  13860  xpccatid  14011  oduval  14283  oppgmnd  14876  lsmmod2  15034  efgi0  15078  efgi1  15079  efginvrel2  15085  efgsval2  15091  efgsp1  15095  efgredleme  15101  efgredlemc  15103  efgcpbllemb  15113  frgpnabllem1  15210  lt6abl  15230  gsumsn  15269  gsum2d  15272  pwsgsum  15279  dprd0  15315  dprdf1  15317  dprd2da  15326  ablfac1lem  15352  pgpfac1lem3  15361  pgpfaclem1  15365  opprrng  15462  mulgass3  15468  ply1assa  16327  ply1coe  16417  zlmval  16526  znbas  16553  znzrh2  16555  restin  16953  imacmp  17180  concompcon  17214  uptx  17375  cnpflf2  17747  tmdgsum2  17831  tsmsres  17878  tsmsf1o  17879  tsmsmhm  17880  prdsxmet  17985  resspwsds  17988  prdsxmslem2  18127  metdcn2  18396  metdcn  18397  metdscn2  18413  iimulcn  18489  icchmeo  18492  xrhmeo  18497  cnrehmeo  18504  cnheiborlem  18505  evth  18510  evth2  18511  lebnumlem2  18513  reparphti  18548  pcoass  18575  pi1xfrcnv  18608  ipcau2  18717  minveclem4  18849  pjthlem1  18854  ovolunlem1a  18908  unmbl  18948  uniioombl  18997  iblitg  19176  dfitg  19177  itg0  19187  iblcnlem1  19195  itgcnlem  19197  itgabs  19242  limcdif  19279  limccnp  19294  limccnp2  19295  dvexp  19355  dvmptid  19359  dvmptc  19360  dvmptfsum  19375  dveflem  19379  dvsincos  19381  mvth  19392  dvlipcn  19394  dvivthlem1  19408  dvfsumle  19421  dvfsumlem2  19427  itgsubst  19449  evlsval  19456  mpff  19478  tdeglem4  19499  tdeglem2  19500  plypf1  19647  plymullem1  19649  coesub  19691  dgrmulc  19705  fta1lem  19740  vieta1lem1  19743  vieta1lem2  19744  aalioulem4  19768  aaliou3lem3  19777  abelthlem2  19861  abelthlem8  19868  abelthlem9  19869  sinhalfpilem  19887  efhalfpi  19892  cospi  19893  efipi  19894  sin2pi  19896  cos2pi  19897  ef2pi  19898  sin2pim  19906  cos2pim  19907  sinmpi  19908  cosmpi  19909  sinppi  19910  cosppi  19911  sincosq4sgn  19922  tangtx  19926  sincos4thpi  19934  sincos6thpi  19936  sincos3rdpi  19937  pige3  19938  abssinper  19939  efif1olem4  19960  efifo  19962  eff1o  19964  logneg  19994  logimul  20021  logneg2  20022  dvrelog  20037  logcnlem4  20045  dvlog  20051  dvlog2  20053  logtayl  20060  1cxp  20072  ecxp  20073  cxpsqr  20103  dvsqr  20137  root1eq1  20148  cxpeq  20150  ang180lem1  20160  ang180lem2  20161  1cubrlem  20190  1cubr  20191  dcubic2  20193  mcubic  20196  cubic2  20197  binom4  20199  dquartlem1  20200  dquartlem2  20201  dquart  20202  quart1lem  20204  quart1  20205  quartlem1  20206  asinsin  20241  asin1  20243  acos1  20244  atanlogsublem  20264  atanlogsub  20265  efiatan2  20266  2efiatan  20267  tanatan  20268  atanbnd  20275  atan1  20277  dvatan  20284  atantayl2  20287  leibpilem2  20290  leibpi  20291  log2cnv  20293  log2tlbnd  20294  log2ublem1  20295  log2ublem2  20296  log2ublem3  20297  log2ub  20298  birthday  20302  amgmlem  20337  emcllem5  20346  wilthlem2  20360  ftalem6  20368  basellem2  20372  basellem3  20373  basellem5  20375  basellem8  20378  cht1  20456  chp1  20458  1sgmprm  20491  ppiublem2  20495  ppiub  20496  chtublem  20503  chtub  20504  logfacbnd3  20515  bcp1ctr  20571  bclbnd  20572  bposlem1  20576  bposlem4  20579  bposlem6  20581  bposlem8  20583  bposlem9  20584  lgslem1  20588  lgsdir2lem1  20615  lgsdir2lem2  20616  lgsdir2lem3  20617  lgsdir2lem5  20619  lgs1  20630  lgseisenlem1  20641  lgseisenlem3  20643  lgsquadlem1  20646  lgsquadlem2  20647  lgsquad2lem2  20651  m1lgs  20654  2sqlem8  20664  2sqblem  20669  logdivsum  20735  mulog2sumlem2  20737  log2sumbnd  20746  selberglem1  20747  selberglem2  20748  pntrmax  20766  pntibndlem2  20793  pntibndlem3  20794  pntlemg  20800  pntlemr  20804  pntlemo  20809  ostth2lem3  20837  ostth2lem4  20838  smcnlem  21325  ipidsq  21341  dipcj  21345  dip0r  21348  nmlnoubi  21429  nmblolbii  21432  blocnilem  21437  ip1ilem  21459  ip2i  21461  ipdirilem  21462  ipasslem10  21472  ipasslem11  21473  siilem1  21484  hvmul0  21658  hvsubsub4i  21693  hvnegdii  21696  hvsubeq0i  21697  hvsubcan2i  21698  hvsubaddi  21700  hvsub0  21710  hisubcomi  21738  normlem0  21743  normlem1  21744  normlem2  21745  normlem3  21746  normlem9  21752  norm-ii-i  21771  norm3difi  21781  normpari  21788  polid2i  21791  polidi  21792  bcsiALT  21813  pjhthlem1  22025  chdmm3i  22113  chdmm4i  22114  chjidm  22154  chj4i  22157  chjjdiri  22158  spanunsni  22213  pjoml4i  22221  cmcm2i  22227  qlax4i  22264  qlax5i  22265  pjadjii  22308  pjmulii  22311  pjsubii  22312  pjssmii  22315  pjcji  22318  pjneli  22357  hoadd32i  22413  ho0subi  22430  hosubid1  22433  hosd2i  22458  hopncani  22459  hosubeq0i  22461  lnopeq0lem1  22640  lnopunilem1  22645  lnophmlem2  22652  nmbdoplbi  22659  nmcopexi  22662  lnfnmuli  22679  nmcfnexi  22686  nmoptri2i  22734  nmopcoadji  22736  golem1  22906  mdsl1i  22956  cvmdi  22959  mdslmd3i  22967  csmdsymi  22969  xrge00  23346  gsumconstf  23359  raddcn  23384  xrge0iifhom  23392  xrge0mulc1cn  23396  cbvesum  23614  gsumesum  23627  esumpfinvallem  23640  esumpfinvalf  23642  dya2icoseg  23801  orrvcval4  23896  orrvcoel  23897  orrvccel  23898  coinflipprob  23911  coinflippvt  23916  ballotlem2  23920  ballotth  23969  subfacp1lem1  23994  subfacp1lem5  23999  subfacval2  24002  subfaclim  24003  subfacval3  24004  cvxpcon  24057  cvxscon  24058  vdgr1c  24180  vdegp1ai  24192  vdegp1bi  24193  vdegp1ci  24194  sinccvglem  24289  4bc3eq4  24384  4bc2eq6  24385  faclimlem1  24481  frrlem5  24670  ax5seglem7  24949  axlowdimlem4  24959  axlowdimlem16  24971  bpoly0  25171  bpoly1  25172  bpolydiflem  25175  bpoly2  25178  bpoly3  25179  bpoly4  25180  fsumcube  25181  itgaddnclem2  25324  itgabsnc  25334  dvreasin  25340  areacirclem2  25342  areacirclem5  25346  areacirc  25348  prdstotbnd  25666  prdsbnd2  25667  repwsmet  25706  rrnequiv  25707  reheibor  25711  mapfzcons  25941  mapfzcons1cl  25943  2rexfrabdioph  26025  3rexfrabdioph  26026  4rexfrabdioph  26027  6rexfrabdioph  26028  7rexfrabdioph  26029  rabdiophlem2  26031  diophren  26044  rabren3dioph  26046  pellexlem5  26066  pell1qr1  26104  rmspecfund  26142  jm2.17a  26195  jm2.17b  26196  jm2.27c  26248  jm2.27dlem5  26254  lmhmlnmsplit  26333  dsmmval2  26350  psgnunilem2  26566  psgnunilem4  26568  psgnpmtr  26581  lhe4.4ex1a  26694  expgrowthi  26698  expgrowth  26700  refsumcn  26849  m1expeven  26873  dvcosre  26889  itgsin0pilem1  26892  itgsinexplem1  26896  stoweidlem13  26910  wallispilem4  26965  wallispi2lem1  26968  wallispi2lem2  26969  stirlinglem1  26971  nn0n0n1ge2  27267  fzo0to2pr  27271  fzo0to3tp  27272  fzo0to42pr  27273  0wlk  27457  0trl  27458  wlkntrllem3  27463  wlkntrllem4  27464  constr1trl  27484  1pthonlem1  27485  2trllem3  27492  constr2trl  27494  wlkdvspthlem  27503  usgrcyclnl2  27525  constr3trllem3  27536  constr3trllem4  27537  constr3trllem5  27538  constr3pthlem1  27539  constr3pthlem3  27541  vdgre1c  27572  sec0  27679  elogb  27708  dalem-cly  29678  pmodN  29857  cdleme0cp  30221  cdleme0cq  30222  cdleme1  30234  cdleme3d  30238  cdleme3h  30242  cdleme4  30245  cdleme5  30247  cdleme7a  30250  cdleme8  30257  cdleme9  30260  cdleme10  30261  cdleme11g  30272  cdleme15b  30282  cdleme21  30344  cdleme22e  30351  cdleme22eALTN  30352  cdleme23c  30358  cdleme25cv  30365  cdleme35b  30457  cdleme35c  30458  cdleme42a  30478  cdleme42d  30480  cdleme43aN  30496  cdlemeg46gfv  30537  cdlemk35  30919  dihjatcclem1  31426  lcdval2  31598  mapdpglem21  31700
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-rex 2583  df-rab 2586  df-v 2824  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-br 4061  df-iota 5256  df-fv 5300  df-ov 5903
  Copyright terms: Public domain W3C validator