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

Theorem oveq1i 6291
Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
Hypothesis
Ref Expression
oveq1i.1  |-  A  =  B
Assertion
Ref Expression
oveq1i  |-  ( A F C )  =  ( B F C )

Proof of Theorem oveq1i
StepHypRef Expression
1 oveq1i.1 . 2  |-  A  =  B
2 oveq1 6288 . 2  |-  ( A  =  B  ->  ( A F C )  =  ( B F C ) )
31, 2ax-mp 5 1  |-  ( A F C )  =  ( B F C )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1383  (class class class)co 6281
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-iota 5541  df-fv 5586  df-ov 6284
This theorem is referenced by:  caov12  6488  caov411  6492  omopthlem1  7306  map1  7596  pw2eng  7625  fsuppunbi  7852  cnfcomlem  8146  cnfcom2  8149  cnfcomlemOLD  8154  cnfcom2OLD  8157  infxpenc2  8402  infxpenc2OLD  8406  adderpqlem  9335  addassnq  9339  distrnq  9342  halfnq  9357  archnq  9361  addclprlem2  9398  addcmpblnr  9449  ltsrpr  9457  m1m1sr  9473  recexsrlem  9483  sqgt0sr  9486  map2psrpr  9490  axi2m1  9539  axcnre  9544  mul02lem2  9760  addid1  9763  cnegex2  9765  addid2  9766  mvlladdi  9842  negsubdi  9880  mulneg1  10000  recextlem1  10186  recdiv  10257  divmul13i  10312  mvllmuli  10384  2p2e4  10660  2times  10661  3p2e5  10675  3p3e6  10676  4p2e6  10677  4p3e7  10678  4p4e8  10679  5p2e7  10680  5p3e8  10681  5p4e9  10682  5p5e10  10683  6p2e8  10684  6p3e9  10685  6p4e10  10686  7p2e9  10687  7p3e10  10688  8p2e10  10689  1mhlfehlf  10765  8th4div3  10766  halfpm6th  10767  nneo  10953  uzindOLD  10964  num0h  10996  numsuc  10998  dec10p  11015  numma  11017  nummac  11018  numma2c  11019  numadd  11020  numaddc  11021  nummul2c  11023  decaddci  11031  decbin0  11089  decbin2  11090  xmulm1  11484  xadddi2  11500  x2times  11502  elfzp1b  11766  elfzm1b  11767  quoremz  11964  quoremnn0ALT  11966  uzrdgxfr  12059  mulexpz  12188  expaddz  12192  sqrecii  12232  cu2  12248  i3  12251  iexpcyc  12254  binom2i  12259  binom2aiOLD  12260  binom3  12269  crreczi  12273  discr  12285  nn0opthlem1  12330  nn0opth2i  12333  faclbnd  12350  bcm1k  12375  bcp1nk  12377  bcpasc  12381  hashp1i  12450  hashxplem  12473  hashpw  12476  hashfun  12477  hashbc  12484  ccatlid  12585  swrdccatin12  12698  revs1  12721  cats1cat  12808  imre  12923  crim  12930  remullem  12943  cnpart  13055  sqrtneglem  13082  absexpz  13120  absimle  13124  sqreulem  13174  amgm2  13184  iseraltlem2  13487  iseraltlem3  13488  modfsummod  13590  binomlem  13623  binom11  13626  arisum  13653  arisum2  13654  georeclim  13663  geo2sum  13664  mertenslem1  13675  mertens  13677  prodfrec  13686  fprodm1s  13756  fprodp1s  13757  efzval  13819  resinval  13852  recosval  13853  efi4p  13854  tan0  13868  efival  13869  sinhval  13871  coshval  13872  cosadd  13882  cos2tsin  13896  ef01bndlem  13901  cos1bnd  13904  cos2bnd  13905  absefib  13915  efieq1re  13916  demoivreALT  13918  eirrlem  13919  rpnnen2lem3  13932  rpnnen2lem11  13940  ruclem7  13951  odd2np1  14028  3dvds  14032  divalglem2  14035  divalglem9  14041  m1bits  14072  sadcp1  14087  sadeq  14104  smupp1  14112  smumul  14125  gcdaddmlem  14148  nn0gcdsq  14267  phiprmpw  14288  prmdiv  14297  prmdiveq  14298  prmdivdiv  14299  pythagtriplem1  14322  pythagtriplem12  14332  pythagtriplem14  14334  pockthi  14407  infpnlem1  14410  prmreclem4  14419  4sqlem12  14456  4sqlem13  14457  4sqlem19  14463  vdwapun  14474  vdwlem6  14486  0hashbc  14507  dec5dvds  14532  dec5nprm  14534  dec2nprm  14535  modxai  14536  modxp1i  14538  mod2xnegi  14539  modsubi  14540  gcdmodi  14542  decexp2  14543  decsplit0b  14548  decsplit1  14550  decsplit  14551  karatsuba  14552  2exp6OLD  14555  2exp8  14556  3exp3  14558  5prm  14576  7prm  14578  11prm  14582  prmlem2  14587  37prm  14588  43prm  14589  83prm  14590  139prm  14591  163prm  14592  317prm  14593  631prm  14594  1259lem1  14595  1259lem2  14596  1259lem3  14597  1259lem4  14598  1259lem5  14599  1259prm  14600  2503lem1  14601  2503lem2  14602  2503lem3  14603  2503prm  14604  4001lem1  14605  4001lem2  14606  4001lem3  14607  4001lem4  14608  4001prm  14609  pwsbas  14866  subsubc  15201  xpccatid  15436  subsubm  15967  mulg2  16130  subsubg  16203  oppgmnd  16368  gsumwrev  16380  psgnunilem2  16499  sylow1lem1  16597  subgslw  16615  sylow3  16632  efginvrel2  16724  efgsfo  16736  frgpnabllem1  16856  gsumzaddlem  16913  gsummptfzsplitl  16932  gsummpt1n0  16971  dprdfid  17036  ablfac1lem  17098  pgpfac1lem3  17107  pgpfaclem1  17111  mgpress  17131  srgbinomlem4  17173  opprring  17259  unitsubm  17298  subsubrg  17434  lsslss  17586  evlsval  18167  mpff  18181  coe1fzgsumdlem  18322  evl1gsumdlem  18371  xrsnsgrp  18433  gzrngunit  18462  expghm  18507  expghmOLD  18508  chrid  18542  zrhpsgnmhm  18598  psgndiflemA  18615  frlmip  18787  frlmphl  18790  matvsca2  18908  mattposvs  18935  m2detleiblem3  19109  m2detleiblem4  19110  cpmidpmat  19352  resstopn  19665  cnmpt1res  20155  ressuss  20744  iscusp2  20783  ucnextcn  20785  txmetcnp  21028  rerest  21287  xrtgioo  21289  xrrest  21290  cnmpt2pc  21406  xrhmeo  21424  reust  21791  rrxprds  21799  csbren  21804  minveclem2  21819  ovolunlem1a  21885  ovolicc2lem4  21909  uniioombllem5  21974  iblabs  22213  iblabsr  22214  iblmulc2  22215  itgmulc2  22218  limcres  22268  dvfval  22279  dvreslem  22291  dvres2lem  22292  dvcnp2  22301  cpnres  22318  dvcobr  22327  dveflem  22358  lhop1lem  22392  lhop2  22394  dvcnvrelem2  22397  plyun0  22572  coeeulem  22599  coeeu  22600  dvply1  22658  dvtaylp  22743  taylthlem2  22747  taylth  22748  dvradcnv  22794  pserdvlem2  22801  abelthlem8  22812  abelth  22814  sinhalfpilem  22834  cospi  22843  eulerid  22845  cos2pi  22847  ef2kpi  22849  sinhalfpip  22863  sinhalfpim  22864  coshalfpip  22865  coshalfpim  22866  sincosq3sgn  22871  sincosq4sgn  22872  tangtx  22876  sincos4thpi  22884  sincos6thpi  22886  sineq0  22892  tanregt0  22904  logm1  22951  abslogle  22981  tanarg  22982  logcnlem4  23004  advlogexp  23014  cxpsqrt  23062  dvsqrt  23096  cxpcn3  23100  root1cj  23108  cxpeq  23109  ang180lem1  23119  ang180lem2  23120  ang180lem3  23121  lawcos  23126  isosctrlem1  23130  isosctrlem2  23131  quad2  23148  1cubrlem  23150  1cubr  23151  dcubic1lem  23152  dcubic2  23153  mcubic  23156  binom4  23159  dquartlem1  23160  quart1lem  23164  quart1  23165  quartlem1  23166  asinlem  23177  asinlem2  23178  asinlem3a  23179  acosneg  23196  efiasin  23197  asinsinlem  23200  asinsin  23201  acoscos  23202  asin1  23203  acosbnd  23209  atancj  23219  efiatan  23221  atanlogaddlem  23222  efiatan2  23226  2efiatan  23227  tanatan  23228  cosatan  23230  atantan  23232  atanbndlem  23234  atans2  23240  dvatan  23244  atantayl  23246  atantayl2  23247  log2cnv  23253  log2tlbnd  23254  log2ublem2  23256  log2ublem3  23257  log2ub  23258  birthday  23262  jensenlem1  23294  amgmlem  23297  wilthlem1  23320  ftalem2  23325  ftalem5  23328  ftalem6  23329  basellem2  23333  basellem3  23334  basellem5  23336  basellem8  23339  basellem9  23340  mule1  23400  ppi1i  23420  musum  23445  ppiublem1  23455  ppiublem2  23456  ppiub  23457  chtublem  23464  chtub  23465  dchrptlem1  23517  dchrptlem2  23518  bclbnd  23533  bpos1  23536  bposlem6  23542  bposlem8  23544  bposlem9  23545  lgslem4  23552  lgsdir2lem1  23576  lgsdir2lem2  23577  lgsdir2lem4  23579  lgsdir2lem5  23580  lgsne0  23586  1lgs  23590  lgseisenlem1  23602  lgseisenlem2  23603  lgseisenlem3  23604  lgseisenlem4  23605  lgseisen  23606  lgsquadlem1  23607  lgsquadlem2  23608  lgsquad2lem1  23611  lgsquad2lem2  23612  m1lgs  23615  chebbnd1lem2  23633  chebbnd1lem3  23634  rplogsumlem2  23648  dchrisum0flblem1  23671  dchrisum0re  23676  mulog2sumlem2  23698  chpdifbndlem1  23716  pntpbnd1a  23748  pntpbnd2  23750  pntibndlem2  23754  pntibndlem3  23755  pntlemg  23761  pntlemk  23769  pntlemo  23770  axsegconlem1  24198  ax5seglem7  24216  axlowdimlem3  24225  axlowdimlem16  24238  axlowdimlem17  24239  usgraexvlem  24373  fargshiftlem  24612  constr3trllem3  24630  eupares  24953  konigsberg  24965  numclwwlk5  25090  numclwwlk7  25092  frgraregord013  25096  ex-fl  25146  ex-ind-dvds  25148  addinv  25332  vc2  25426  vc0  25440  vcm  25442  vcnegneg  25445  nvnncan  25536  nvm1  25545  nvpi  25547  nvmtri  25552  nvge0  25555  ipval3  25597  ipidsq  25601  ip0i  25718  ip1ilem  25719  ip2i  25721  ipdirilem  25722  ipasslem10  25732  siilem1  25744  siii  25746  minvecolem2  25769  hvsubid  25921  hvaddsubval  25928  hvmul2negi  25943  hvadd12i  25952  hv2times  25956  hvnegdii  25957  hvaddcani  25960  hi01  25991  hisubcomi  25999  normlem0  26004  normlem1  26005  normlem3  26007  normlem9  26013  bcseqi  26015  normsqi  26027  norm-ii-i  26032  normsubi  26036  norm3difi  26042  norm3adifii  26043  normpar2i  26051  polid2i  26052  polidi  26053  chdmm2i  26374  chj12i  26418  spanunsni  26475  qlaxr5i  26531  osumcor2i  26540  spansnji  26542  pjadjii  26570  pjinormii  26572  pjsslem  26575  pjpythi  26618  mayete3i  26624  mayete3iOLD  26625  mayetes3i  26626  hoadd12i  26674  honegneg  26703  ho2times  26716  hoaddsubi  26718  hosd1i  26719  hosd2i  26720  honpncani  26724  lnopeq0lem1  26902  lnopunilem1  26907  lnophmlem2  26914  lnfn0i  26939  nmopcoadji  26998  nmopcoadj2i  26999  opsqrlem1  27037  opsqrlem5  27041  opsqrlem6  27042  pjclem3  27094  stadd3i  27145  mddmd2  27206  mdexchi  27232  cvexchlem  27265  atomli  27279  atordi  27281  atabs2i  27299  mdsymlem1  27300  iuninc  27406  suppss3  27528  archirngz  27711  gsumvsca2  27752  nn0omnd  27809  nn0archi  27811  xrge0slmod  27812  sqsscirc1  27868  cnvordtrestixx  27873  raddcn  27889  xrge0iifhom  27897  xrge0mulc1cn  27901  xrge0tmd  27906  lmlimxrge0  27908  qqhucn  27951  rrhcn  27956  logb1  27997  brfae  28198  cndprobnul  28354  isrrvv  28360  ballotlem1  28403  ballotlem2  28405  ballotlemodife  28414  ballotlemi1  28419  ballotlemii  28420  ballotlemic  28423  ballotlem1c  28424  ballotlemfrceq  28445  ballotth  28454  ofcs2  28480  signsvtn0  28505  signstfveq0  28512  signsvtp  28518  signsvtn  28519  signsvfpn  28520  signsvfnn  28521  signshf  28523  lgamgulmlem2  28550  lgamgulmlem5  28553  lgambdd  28557  subfacp1lem1  28601  subfacp1lem5  28606  subfacp1lem6  28607  subfaclim  28610  cvmliftlem5  28712  cvmliftlem8  28715  cvmliftlem10  28717  cvmliftlem13  28719  cvmlift2lem6  28731  cvmlift2lem12  28737  problem1  28997  problem2  28998  problem4  29000  quad3  29002  fallfacfwd  29134  0risefac  29136  bpolydiflem  29792  bpoly2  29795  bpoly3  29796  bpoly4  29797  fsumcube  29798  sin2h  30021  mblfinlem3  30029  ismblfin  30031  itg2addnclem3  30044  iblabsnc  30055  iblmulc2nc  30056  itgmulc2nc  30059  ftc1cnnc  30065  ftc1anclem6  30071  ftc1anclem7  30072  ftc1anclem8  30073  dvcnsqrt  30077  dvasin  30079  fdc  30214  heiborlem4  30286  heiborlem6  30288  pellexlem5  30745  reglog1  30808  jm2.23  30914  jm2.27c  30925  lnmlsslnm  31003  lmhmlnmsplit  31009  cntzsdrg  31127  areaquad  31160  hashnzfz2  31202  lhe4.4ex1a  31210  fzisoeu  31454  fz1ssfz0  31464  fsummulc1f  31523  fprodexp  31554  constlimc  31584  sumnnodd  31590  limcresiooub  31602  limcresioolb  31603  cncfshiftioo  31649  fperdvper  31669  dvnmul  31694  dvmptfprod  31696  itgsinexplem1  31706  stoweidlem11  31747  stoweidlem13  31749  stoweidlem26  31762  stoweidlem34  31770  wallispilem4  31804  wallispi2lem1  31807  wallispi2lem2  31808  stirlinglem11  31820  dirkerper  31832  dirkertrigeqlem1  31834  dirkertrigeqlem3  31836  dirkercncflem1  31839  dirkercncflem4  31842  fourierdlem30  31873  fourierdlem32  31875  fourierdlem33  31876  fourierdlem42  31885  fourierdlem46  31889  fourierdlem47  31890  fourierdlem57  31900  fourierdlem60  31903  fourierdlem61  31904  fourierdlem62  31905  fourierdlem68  31911  fourierdlem73  31916  fourierdlem79  31922  fourierdlem89  31932  fourierdlem90  31933  fourierdlem91  31934  fourierdlem96  31939  fourierdlem97  31940  fourierdlem98  31941  fourierdlem99  31942  fourierdlem100  31943  fourierdlem103  31946  fourierdlem104  31947  fourierdlem108  31951  fourierdlem110  31953  fourierdlem113  31956  sqwvfoura  31965  sqwvfourb  31966  fourierswlem  31967  fouriersw  31968  fouriercn  31969  etransclem4  31975  etransclem7  31978  etransclem23  31994  etransclem24  31995  etransclem25  31996  etransclem26  31997  etransclem28  31999  etransclem31  32002  etransclem32  32003  etransclem35  32006  etransclem37  32008  etransclem46  32017  subsubmgm  32439  altgsumbcALT  32810  lincfsuppcl  32884  linccl  32885  lincvalsn  32888  lincdifsn  32895  lincsum  32900  lincscm  32901  lindslinindimp2lem4  32932  lindslinindsimp2lem5  32933  snlindsntor  32942  lincresunit3lem2  32951  zlmodzxzldeplem3  32973  ldepsnlinc  32979  sinh-conventional  33003  onetansqsecsq  33025  cotsqcscsq  33026  dpfrac1  33036  mvlraddi  33050  mvrladdi  33052  mvrraddi  33054  mvlrmuli  33062  sineq0ALT  33605  dalem24  35296  pmod2iN  35448  cdleme9  35853  cdleme20aN  35910  cdleme22e  35945  cdleme22eALTN  35946  cdleme25cv  35959  cdleme29b  35976  cdlemh1  36416  cdlemh2  36417  cdlemk35  36513  cdlemkid1  36523  inductionexd  37771
  Copyright terms: Public domain W3C validator