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

Theorem oveq1i 6325
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 6322 . 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 1455  (class class class)co 6315
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rex 2755  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-iota 5565  df-fv 5609  df-ov 6318
This theorem is referenced by:  caov12  6524  caov411  6528  omopthlem1  7382  map1  7674  pw2eng  7704  fsuppunbi  7930  cnfcomlem  8230  cnfcom2  8233  infxpenc2  8479  adderpqlem  9405  addassnq  9409  distrnq  9412  halfnq  9427  archnq  9431  addclprlem2  9468  addcmpblnr  9519  ltsrpr  9527  m1m1sr  9543  recexsrlem  9553  sqgt0sr  9556  map2psrpr  9560  axi2m1  9609  axcnre  9614  mul02lem2  9836  addid1  9839  cnegex2  9841  addid2  9842  mvlladdi  9918  negsubdi  9956  mulneg1  10083  recextlem1  10270  recdiv  10341  divmul13i  10396  mvllmuli  10468  2p2e4  10756  2times  10757  3p2e5  10771  3p3e6  10772  4p2e6  10773  4p3e7  10774  4p4e8  10775  5p2e7  10776  5p3e8  10777  5p4e9  10778  5p5e10  10779  6p2e8  10780  6p3e9  10781  6p4e10  10782  7p2e9  10783  7p3e10  10784  8p2e10  10785  1mhlfehlf  10861  8th4div3  10862  halfpm6th  10863  nneo  11048  num0h  11090  numsuc  11092  dec10p  11109  numma  11111  nummac  11112  numma2c  11113  numadd  11114  numaddc  11115  nummul2c  11117  decaddci  11125  decbin0  11183  decbin2  11184  xmulm1  11596  xadddi2  11612  x2times  11614  elfzp1b  11900  elfzm1b  11901  fz1fzo0m1  11994  quoremz  12114  quoremnn0ALT  12116  uzrdgxfr  12212  mulexpz  12344  expaddz  12348  sqrecii  12389  cu2  12405  i3  12408  iexpcyc  12411  binom2i  12416  binom3  12425  crreczi  12429  discr  12441  nn0opthlem1  12486  nn0opth2i  12489  faclbnd  12507  bcm1k  12532  bcp1nk  12534  bcpasc  12538  hashp1i  12612  hashxplem  12638  hashpw  12641  hashfun  12642  hashbc  12649  ccatlid  12766  swrdccatin12  12884  revs1  12907  cats1cat  12994  lsws2  13035  lsws3  13036  lsws4  13037  imre  13220  crim  13227  remullem  13240  cnpart  13352  sqrtneglem  13379  absexpz  13417  absimle  13421  sqreulem  13471  amgm2  13481  iseraltlem2  13798  iseraltlem3  13799  modfsummod  13903  binomlem  13936  binom11  13939  arisum  13967  arisum2  13968  georeclim  13977  geo2sum  13978  mertenslem1  13989  mertens  13991  prodfrec  14000  fprodm1s  14073  fprodp1s  14074  fallfacfwd  14138  0risefac  14140  bpolydiflem  14156  bpoly2  14159  bpoly3  14160  bpoly4  14161  fsumcube  14162  efzval  14205  resinval  14238  recosval  14239  efi4p  14240  tan0  14254  efival  14255  sinhval  14257  coshval  14258  cosadd  14268  cos2tsin  14282  ef01bndlem  14287  cos1bnd  14290  cos2bnd  14291  absefib  14301  efieq1re  14302  demoivreALT  14304  eirrlem  14305  rpnnen2lem3  14318  rpnnen2lem11  14326  ruclem7  14337  odd2np1  14414  3dvds  14418  divalglem2  14422  divalglem2OLD  14423  divalglem9  14430  divalglem9OLD  14431  m1bits  14463  sadcp1  14478  sadeq  14495  smupp1  14503  smumul  14516  gcdaddmlem  14541  3lcm2e6woprm  14629  nn0gcdsq  14750  phiprmpw  14773  prmdiv  14782  prmdiveq  14783  prmdivdiv  14784  pythagtriplem1  14815  pythagtriplem12  14825  pythagtriplem14  14827  pockthi  14900  infpnlem1  14903  prmreclem4  14912  4sqlem12  14949  4sqlem13OLD  14950  4sqlem13  14956  4sqlem19  14962  vdwapun  14973  vdwlem6  14985  0hashbc  15008  prmo2  15047  prmo3  15048  dec5dvds  15085  dec5nprm  15087  dec2nprm  15088  modxai  15089  modxp1i  15091  mod2xnegi  15092  modsubi  15093  gcdmodi  15095  decexp2  15096  decsplit0b  15101  decsplit1  15103  decsplit  15104  karatsuba  15105  2exp6OLD  15108  2exp8  15109  3exp3  15111  5prm  15129  7prm  15131  11prm  15135  prmlem2  15140  37prm  15141  43prm  15142  83prm  15143  139prm  15144  163prm  15145  317prm  15146  631prm  15147  prmo5  15149  1259lem1  15151  1259lem2  15152  1259lem3  15153  1259lem4  15154  1259lem5  15155  1259prm  15156  2503lem1  15157  2503lem2  15158  2503lem3  15159  2503prm  15160  4001lem1  15161  4001lem2  15162  4001lem3  15163  4001lem4  15164  4001prm  15165  pwsbas  15434  rcaninv  15748  subsubc  15807  xpccatid  16122  subsubm  16653  mulg2  16816  subsubg  16889  oppgmnd  17054  gsumwrev  17066  psgnunilem2  17185  sylow1lem1  17299  subgslw  17317  sylow3  17334  efginvrel2  17426  efgsfo  17438  frgpnabllem1  17558  gsumzaddlem  17603  gsummptfzsplitl  17615  gsummpt1n0  17646  dprdfid  17699  ablfac1lem  17750  pgpfac1lem3  17759  pgpfaclem1  17763  mgpress  17783  srgbinomlem4  17825  opprring  17908  unitsubm  17947  subsubrg  18083  lsslss  18233  evlsval  18791  mpff  18805  coe1fzgsumdlem  18944  evl1gsumdlem  18993  xrsnsgrp  19053  gzrngunit  19082  expghm  19116  chrid  19147  zrhpsgnmhm  19201  psgndiflemA  19218  frlmip  19385  frlmphl  19388  matvsca2  19502  mattposvs  19529  m2detleiblem3  19703  m2detleiblem4  19704  cpmidpmat  19946  resstopn  20251  cnmpt1res  20740  ressuss  21327  iscusp2  21366  ucnextcn  21368  txmetcnp  21611  rerest  21871  xrtgioo  21873  xrrest  21874  cnmpt2pc  22005  xrhmeo  22023  reust  22389  rrxprds  22397  csbren  22402  minveclem2  22417  minveclem2OLD  22429  ovolunlem1a  22498  ovolicc2lem4OLD  22522  ovolicc2lem4  22523  uniioombllem5  22594  iblabs  22835  iblabsr  22836  iblmulc2  22837  itgmulc2  22840  limcres  22890  dvfval  22901  dvreslem  22913  dvres2lem  22914  dvcnp2  22923  cpnres  22940  dvcobr  22949  dveflem  22980  lhop1lem  23014  lhop2  23016  dvcnvrelem2  23019  plyun0  23200  coeeulem  23227  coeeu  23228  dvply1  23286  dvtaylp  23374  taylthlem2  23378  taylth  23379  dvradcnv  23425  pserdvlem2  23432  abelthlem8  23443  abelth  23445  sinhalfpilem  23467  cospi  23476  eulerid  23478  cos2pi  23480  ef2kpi  23482  sinhalfpip  23496  sinhalfpim  23497  coshalfpip  23498  coshalfpim  23499  sincosq3sgn  23504  sincosq4sgn  23505  tangtx  23509  sincos4thpi  23517  sincos6thpi  23519  sineq0  23525  tanregt0  23537  logm1  23587  abslogle  23616  tanarg  23617  logcnlem4  23639  advlogexp  23649  cxpsqrt  23697  dvsqrt  23731  dvcnsqrt  23733  cxpcn3  23737  root1cj  23745  cxpeq  23746  logb1  23755  ang180lem1  23787  ang180lem2  23788  ang180lem3  23789  lawcos  23794  isosctrlem1  23796  isosctrlem2  23797  quad2  23814  1cubrlem  23816  1cubr  23817  dcubic1lem  23818  dcubic2  23819  mcubic  23822  binom4  23825  dquartlem1  23826  quart1lem  23830  quart1  23831  quartlem1  23832  asinlem  23843  asinlem2  23844  asinlem3a  23845  acosneg  23862  efiasin  23863  asinsinlem  23866  asinsin  23867  acoscos  23868  asin1  23869  acosbnd  23875  atancj  23885  efiatan  23887  atanlogaddlem  23888  efiatan2  23892  2efiatan  23893  tanatan  23894  cosatan  23896  atantan  23898  atanbndlem  23900  atans2  23906  dvatan  23910  atantayl  23912  atantayl2  23913  log2cnv  23919  log2tlbnd  23920  log2ublem2  23922  log2ublem3  23923  log2ub  23924  birthday  23929  jensenlem1  23961  amgmlem  23964  lgamgulmlem2  24004  lgamgulmlem5  24007  lgambdd  24011  wilthlem1  24042  ftalem2  24047  ftalem5  24050  ftalem5OLD  24052  ftalem6  24053  basellem2  24057  basellem3  24058  basellem5  24060  basellem8  24063  basellem9  24064  mule1  24124  ppi1i  24144  musum  24169  ppiublem1  24179  ppiublem2  24180  ppiub  24181  chtublem  24188  chtub  24189  dchrptlem1  24241  dchrptlem2  24242  bclbnd  24257  bpos1  24260  bposlem6  24266  bposlem8  24268  bposlem9  24269  lgslem4  24276  lgsdir2lem1  24300  lgsdir2lem2  24301  lgsdir2lem4  24303  lgsdir2lem5  24304  lgsne0  24310  1lgs  24314  lgseisenlem1  24326  lgseisenlem2  24327  lgseisenlem3  24328  lgseisenlem4  24329  lgseisen  24330  lgsquadlem1  24331  lgsquadlem2  24332  lgsquad2lem1  24335  lgsquad2lem2  24336  m1lgs  24339  chebbnd1lem2  24357  chebbnd1lem3  24358  rplogsumlem2  24372  dchrisum0flblem1  24395  dchrisum0re  24400  mulog2sumlem2  24422  chpdifbndlem1  24440  pntpbnd1a  24472  pntpbnd2  24474  pntibndlem2  24478  pntibndlem3  24479  pntlemg  24485  pntlemk  24493  pntlemo  24494  axsegconlem1  24996  ax5seglem7  25014  axlowdimlem3  25023  axlowdimlem16  25036  axlowdimlem17  25037  usgraexmplvtxlem  25171  fargshiftlem  25411  constr3trllem3  25429  eupares  25752  konigsberg  25764  numclwwlk5  25889  numclwwlk7  25891  frgraregord013  25895  ex-fl  25946  ex-ind-dvds  25948  addinv  26129  vc2  26223  vc0  26237  vcm  26239  vcnegneg  26242  nvnncan  26333  nvm1  26342  nvpi  26344  nvmtri  26349  nvge0  26352  ipval3  26394  ipidsq  26398  ip0i  26515  ip1ilem  26516  ip2i  26518  ipdirilem  26519  ipasslem10  26529  siilem1  26541  siii  26543  minvecolem2  26566  minvecolem2OLD  26576  hvsubid  26728  hvaddsubval  26735  hvmul2negi  26750  hvadd12i  26759  hv2times  26763  hvnegdii  26764  hvaddcani  26767  hi01  26798  hisubcomi  26806  normlem0  26811  normlem1  26812  normlem3  26814  normlem9  26820  bcseqi  26822  normsqi  26834  norm-ii-i  26839  normsubi  26843  norm3difi  26849  norm3adifii  26850  normpar2i  26858  polid2i  26859  polidi  26860  chdmm2i  27180  chj12i  27224  spanunsni  27281  qlaxr5i  27337  osumcor2i  27346  spansnji  27348  pjadjii  27376  pjinormii  27378  pjsslem  27381  pjpythi  27424  mayete3i  27430  mayetes3i  27431  hoadd12i  27479  honegneg  27508  ho2times  27521  hoaddsubi  27523  hosd1i  27524  hosd2i  27525  honpncani  27529  lnopeq0lem1  27707  lnopunilem1  27712  lnophmlem2  27719  lnfn0i  27744  nmopcoadji  27803  nmopcoadj2i  27804  opsqrlem1  27842  opsqrlem5  27846  opsqrlem6  27847  pjclem3  27899  stadd3i  27950  mddmd2  28011  mdexchi  28037  cvexchlem  28070  atomli  28084  atordi  28086  atabs2i  28104  mdsymlem1  28105  iuninc  28225  suppss2f  28287  suppss3  28361  archirngz  28555  gsumvsca2  28595  nn0omnd  28653  nn0archi  28655  xrge0slmod  28656  lmatfvlem  28690  sqsscirc1  28763  cnvordtrestixx  28768  raddcn  28784  xrge0iifhom  28792  xrge0mulc1cn  28796  xrge0tmd  28801  lmlimxrge0  28803  qqhucn  28845  rrhcn  28850  qqtopn  28864  rrhqima  28867  brfae  29120  inelcarsg  29192  cndprobnul  29319  isrrvv  29325  ballotlem1  29368  ballotlem2  29370  ballotlemodife  29379  ballotlemi1  29384  ballotlemii  29385  ballotlemic  29388  ballotlem1c  29389  ballotlemfrceq  29410  ballotth  29419  ballotlemi1OLD  29422  ballotlemiiOLD  29423  ballotlemicOLD  29426  ballotlem1cOLD  29427  ballotlemfrceqOLD  29448  ballotthOLD  29457  ofcs2  29483  signsvtn0  29508  signstfveq0  29515  signsvtp  29521  signsvtn  29522  signsvfpn  29523  signsvfnn  29524  signshf  29526  subfacp1lem1  29951  subfacp1lem5  29956  subfacp1lem6  29957  subfaclim  29960  cvmliftlem5  30061  cvmliftlem8  30064  cvmliftlem10  30066  cvmliftlem13  30068  cvmlift2lem6  30080  cvmlift2lem12  30086  problem1  30346  problem2  30347  problem4  30349  quad3  30351  iexpire  30420  sin2h  31980  poimirlem16  32001  poimirlem17  32002  poimirlem18  32003  poimirlem19  32004  poimirlem20  32005  poimirlem21  32006  poimirlem22  32007  poimirlem26  32011  mblfinlem3  32024  ismblfin  32026  itg2addnclem3  32040  iblabsnc  32051  iblmulc2nc  32052  itgmulc2nc  32055  ftc1cnnc  32061  ftc1anclem6  32067  ftc1anclem7  32068  ftc1anclem8  32069  dvasin  32073  fdc  32119  heiborlem4  32191  heiborlem6  32193  dalem24  33307  pmod2iN  33459  cdleme9  33864  cdleme20aN  33921  cdleme22e  33956  cdleme22eALTN  33957  cdleme25cv  33970  cdleme29b  33987  cdlemh1  34427  cdlemh2  34428  cdlemk35  34524  cdlemkid1  34534  pellexlem5  35722  reglog1  35789  jm2.23  35896  jm2.27c  35907  lnmlsslnm  35984  lmhmlnmsplit  35990  cntzsdrg  36113  areaquad  36146  cotrclrcl  36379  inductionexd  36638  hashnzfz2  36714  lhe4.4ex1a  36722  binomcxplemdvsum  36748  binomcxplemnotnn0  36749  binomcxp  36750  sineq0ALT  37374  fzisoeu  37556  fz1ssfz0  37566  fsummulc1f  37685  fprodexp  37712  constlimc  37742  sumnnodd  37748  limcresiooub  37761  limcresioolb  37762  cncfshiftioo  37808  fperdvper  37828  dvnmul  37856  dvmptfprod  37858  itgsinexplem1  37868  stoweidlem11  37909  stoweidlem13  37911  stoweidlem26  37924  stoweidlem34  37933  wallispilem4  37968  wallispi2lem1  37971  wallispi2lem2  37972  stirlinglem11  37984  dirkerper  37996  dirkertrigeqlem1  37998  dirkertrigeqlem3  38000  dirkercncflem1  38003  dirkercncflem4  38006  fourierdlem30  38037  fourierdlem32  38040  fourierdlem33  38041  fourierdlem42  38050  fourierdlem42OLD  38051  fourierdlem46  38054  fourierdlem47  38055  fourierdlem57  38065  fourierdlem60  38068  fourierdlem61  38069  fourierdlem62  38070  fourierdlem68  38076  fourierdlem73  38081  fourierdlem79  38087  fourierdlem89  38097  fourierdlem90  38098  fourierdlem91  38099  fourierdlem96  38104  fourierdlem97  38105  fourierdlem98  38106  fourierdlem99  38107  fourierdlem100  38108  fourierdlem103  38111  fourierdlem104  38112  fourierdlem108  38116  fourierdlem110  38118  fourierdlem113  38121  sqwvfoura  38130  sqwvfourb  38131  fourierswlem  38132  fouriersw  38133  fouriercn  38134  etransclem4  38141  etransclem7  38144  etransclem23  38160  etransclem24  38161  etransclem25  38162  etransclem26  38163  etransclem31  38168  etransclem32  38169  etransclem35  38172  etransclem37  38174  etransclem46  38183  rrxdsfi  38192  rrndistlt  38197  sge0tsms  38260  sge0xaddlem2  38314  1t10e1p1e11  38748  deccarry  38753  1fzopredsuc  38759  m1mod0mod1  38761  iccpartgt  38779  m1expevenALTV  38815  1oddALTV  38857  6even  38876  8even  38878  gbpart7  38906  gbpart9  38908  gbpart11  38909  bgoldbtbndlem1  38938  tgoldbachlt  38947  3exp4mod41  38954  41prothprmlem1  38955  41prothprmlem2  38956  41prothprm  38957  pfxccatin12  39006  elfz0lmr  39112  sPthisPth  39760  21wlkdlem1  39874  2pthd  39889  31wlkdlem1  39900  3pthd  39915  subsubmgm  40070  altgsumbcALT  40407  lincfsuppcl  40479  linccl  40480  lincvalsn  40483  lincdifsn  40490  lincsum  40495  lincscm  40496  lindslinindimp2lem4  40527  lindslinindsimp2lem5  40528  snlindsntor  40537  lincresunit3lem2  40546  zlmodzxzldeplem3  40568  ldepsnlinc  40574  nn0o1gt2  40600  nn0o  40602  nn0sumshdiglemA  40703  nn0sumshdiglemB  40704  sinh-conventional  40732  onetansqsecsq  40754  cotsqcscsq  40755  dpfrac1  40765  mvlraddi  40777  mvrladdi  40779  mvrraddi  40781  mvlrmuli  40789
  Copyright terms: Public domain W3C validator