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

Theorem oveq1i 6090
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 6087 . 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 1362  (class class class)co 6080
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-iota 5369  df-fv 5414  df-ov 6083
This theorem is referenced by:  caov12  6280  caov411  6284  omopthlem1  7082  map1  7376  pw2eng  7405  fsuppunbi  7629  cnfcomlem  7920  cnfcom2  7923  cnfcomlemOLD  7928  cnfcom2OLD  7931  infxpenc2  8176  infxpenc2OLD  8180  adderpqlem  9111  addassnq  9115  distrnq  9118  halfnq  9133  archnq  9137  addclprlem2  9174  addcmpblnr  9227  ltsrpr  9232  m1m1sr  9248  recexsrlem  9258  sqgt0sr  9261  map2psrpr  9265  axi2m1  9314  axcnre  9319  mul02lem2  9534  addid1  9537  cnegex2  9539  addid2  9540  mvlladdi  9615  negsubdi  9653  mulneg1  9769  recextlem1  9954  recdiv  10025  divmul13i  10080  mvllmuli  10152  2p2e4  10427  2times  10428  3p2e5  10442  3p3e6  10443  4p2e6  10444  4p3e7  10445  4p4e8  10446  5p2e7  10447  5p3e8  10448  5p4e9  10449  5p5e10  10450  6p2e8  10451  6p3e9  10452  6p4e10  10453  7p2e9  10454  7p3e10  10455  8p2e10  10456  1mhlfehlf  10532  8th4div3  10533  halfpm6th  10534  nneo  10713  uzindOLD  10724  num0h  10753  numsuc  10755  dec10p  10772  numma  10774  nummac  10775  numma2c  10776  numadd  10777  numaddc  10778  nummul2c  10780  decaddci  10788  decbin0  10846  decbin2  10847  xmulm1  11232  xadddi2  11248  x2times  11250  elfzp1b  11521  elfzm1b  11522  quoremz  11678  quoremnn0ALT  11680  uzrdgxfr  11773  mulexpz  11888  expaddz  11892  sqrecii  11932  cu2  11948  i3  11951  iexpcyc  11954  binom2i  11959  binom2aiOLD  11960  binom3  11969  crreczi  11973  discr  11985  nn0opthlem1  12030  nn0opth2i  12033  faclbnd  12050  bcm1k  12075  bcp1nk  12077  bcpasc  12081  hashp1i  12145  hashxplem  12179  hashpw  12182  hashfun  12183  hashbc  12190  ccatlid  12268  swrdccatin12  12366  revs1  12389  cats1cat  12472  imre  12581  crim  12588  remullem  12601  cnpart  12713  sqrneglem  12740  absexpz  12778  absimle  12782  sqreulem  12831  amgm2  12841  iseraltlem2  13144  iseraltlem3  13145  binomlem  13275  binom11  13278  arisum  13305  arisum2  13306  georeclim  13315  geo2sum  13316  mertenslem1  13327  mertens  13329  efzval  13369  resinval  13402  recosval  13403  efi4p  13404  tan0  13418  efival  13419  sinhval  13421  coshval  13422  cosadd  13432  cos2tsin  13446  ef01bndlem  13451  cos1bnd  13454  cos2bnd  13455  absefib  13465  efieq1re  13466  demoivreALT  13468  eirrlem  13469  rpnnen2lem3  13482  rpnnen2lem11  13490  ruclem7  13501  odd2np1  13575  3dvds  13579  divalglem2  13582  divalglem9  13588  m1bits  13619  sadcp1  13634  sadeq  13651  smupp1  13659  smumul  13672  gcdaddmlem  13695  nn0gcdsq  13813  phiprmpw  13834  prmdiv  13843  prmdiveq  13844  prmdivdiv  13845  pythagtriplem1  13866  pythagtriplem12  13876  pythagtriplem14  13878  pockthi  13951  infpnlem1  13954  prmreclem4  13963  4sqlem12  14000  4sqlem13  14001  4sqlem19  14007  vdwapun  14018  vdwlem6  14030  0hashbc  14051  dec5dvds  14076  dec5nprm  14078  dec2nprm  14079  modxai  14080  modxp1i  14082  mod2xnegi  14083  modsubi  14084  gcdmodi  14086  decexp2  14087  decsplit0b  14092  decsplit1  14094  decsplit  14095  karatsuba  14096  2exp6  14098  2exp8  14099  3exp3  14101  5prm  14119  7prm  14121  11prm  14125  prmlem2  14130  37prm  14131  43prm  14132  83prm  14133  139prm  14134  163prm  14135  317prm  14136  631prm  14137  1259lem1  14138  1259lem2  14139  1259lem3  14140  1259lem4  14141  1259lem5  14142  1259prm  14143  2503lem1  14144  2503lem2  14145  2503lem3  14146  2503prm  14147  4001lem1  14148  4001lem2  14149  4001lem3  14150  4001lem4  14151  4001prm  14152  pwsbas  14408  subsubc  14746  xpccatid  14981  subsubm  15467  mulg2  15616  subsubg  15684  oppgmnd  15849  gsumwrev  15861  psgnunilem2  15981  sylow1lem1  16077  subgslw  16095  sylow3  16112  efginvrel2  16204  efgsfo  16216  frgpnabllem1  16331  gsumzaddlem  16388  gsummptif1n0  16431  dprdfid  16481  ablfac1lem  16543  pgpfac1lem3  16552  pgpfaclem1  16556  mgpress  16576  opprrng  16657  unitsubm  16696  subsubrg  16815  lsslss  16964  gzrngunit  17722  expghm  17765  expghmOLD  17766  chrid  17800  zrhpsgnmhm  17856  psgndiflemA  17873  frlmip  18045  frlmphl  18048  matvsca2  18170  mattposvs  18181  m2detleiblem3  18277  m2detleiblem4  18278  resstopn  18632  cnmpt1res  19091  ressuss  19680  iscusp2  19719  ucnextcn  19721  txmetcnp  19964  rerest  20223  xrtgioo  20225  xrrest  20226  cnmpt2pc  20342  xrhmeo  20360  reust  20727  rrxprds  20735  csbren  20740  minveclem2  20755  ovolunlem1a  20821  ovolicc2lem4  20845  uniioombllem5  20909  iblabs  21148  iblabsr  21149  iblmulc2  21150  itgmulc2  21153  limcres  21203  dvfval  21214  dvreslem  21226  dvres2lem  21227  dvcnp2  21236  cpnres  21253  dvcobr  21262  dveflem  21293  lhop1lem  21327  lhop2  21329  dvcnvrelem2  21332  evlsval  21371  mpff  21393  plyun0  21550  coeeulem  21577  coeeu  21578  dvply1  21635  dvtaylp  21720  taylthlem2  21724  taylth  21725  dvradcnv  21771  pserdvlem2  21778  abelthlem8  21789  abelth  21791  sinhalfpilem  21810  cospi  21819  eulerid  21821  cos2pi  21823  ef2kpi  21825  sinhalfpip  21839  sinhalfpim  21840  coshalfpip  21841  coshalfpim  21842  sincosq3sgn  21847  sincosq4sgn  21848  tangtx  21852  sincos4thpi  21860  sincos6thpi  21862  sineq0  21868  tanregt0  21880  logm1  21922  abslogle  21952  tanarg  21953  logcnlem4  21975  advlogexp  21985  cxpsqr  22033  dvsqr  22067  cxpcn3  22071  root1cj  22079  cxpeq  22080  ang180lem1  22090  ang180lem2  22091  ang180lem3  22092  lawcos  22097  isosctrlem1  22101  isosctrlem2  22102  quad2  22119  1cubrlem  22121  1cubr  22122  dcubic1lem  22123  dcubic2  22124  mcubic  22127  binom4  22130  dquartlem1  22131  quart1lem  22135  quart1  22136  quartlem1  22137  asinlem  22148  asinlem2  22149  asinlem3a  22150  acosneg  22167  efiasin  22168  asinsinlem  22171  asinsin  22172  acoscos  22173  asin1  22174  acosbnd  22180  atancj  22190  efiatan  22192  atanlogaddlem  22193  efiatan2  22197  2efiatan  22198  tanatan  22199  cosatan  22201  atantan  22203  atanbndlem  22205  atans2  22211  dvatan  22215  atantayl  22217  atantayl2  22218  log2cnv  22224  log2tlbnd  22225  log2ublem2  22227  log2ublem3  22228  log2ub  22229  birthday  22233  jensenlem1  22265  amgmlem  22268  wilthlem1  22291  ftalem2  22296  ftalem5  22299  ftalem6  22300  basellem2  22304  basellem3  22305  basellem5  22307  basellem8  22310  basellem9  22311  mule1  22371  ppi1i  22391  musum  22416  ppiublem1  22426  ppiublem2  22427  ppiub  22428  chtublem  22435  chtub  22436  dchrptlem1  22488  dchrptlem2  22489  bclbnd  22504  bpos1  22507  bposlem6  22513  bposlem8  22515  bposlem9  22516  lgslem4  22523  lgsdir2lem1  22547  lgsdir2lem2  22548  lgsdir2lem4  22550  lgsdir2lem5  22551  lgsne0  22557  1lgs  22561  lgseisenlem1  22573  lgseisenlem2  22574  lgseisenlem3  22575  lgseisenlem4  22576  lgseisen  22577  lgsquadlem1  22578  lgsquadlem2  22579  lgsquad2lem1  22582  lgsquad2lem2  22583  m1lgs  22586  chebbnd1lem2  22604  chebbnd1lem3  22605  rplogsumlem2  22619  dchrisum0flblem1  22642  dchrisum0re  22647  mulog2sumlem2  22669  chpdifbndlem1  22687  pntpbnd1a  22719  pntpbnd2  22721  pntibndlem2  22725  pntibndlem3  22726  pntlemg  22732  pntlemk  22740  pntlemo  22741  axsegconlem1  22986  ax5seglem7  23004  axlowdimlem3  23013  axlowdimlem16  23026  axlowdimlem17  23027  usgraexvlem  23136  fargshiftlem  23343  constr3trllem3  23361  eupares  23419  konigsberg  23431  ex-fl  23477  addinv  23662  vc2  23756  vc0  23770  vcm  23772  vcnegneg  23775  nvnncan  23866  nvm1  23875  nvpi  23877  nvmtri  23882  nvge0  23885  ipval3  23927  ipidsq  23931  ip0i  24048  ip1ilem  24049  ip2i  24051  ipdirilem  24052  ipasslem10  24062  siilem1  24074  siii  24076  minvecolem2  24099  hvsubid  24251  hvaddsubval  24258  hvmul2negi  24273  hvadd12i  24282  hv2times  24286  hvnegdii  24287  hvaddcani  24290  hi01  24321  hisubcomi  24329  normlem0  24334  normlem1  24335  normlem3  24337  normlem9  24343  bcseqi  24345  normsqi  24357  norm-ii-i  24362  normsubi  24366  norm3difi  24372  norm3adifii  24373  normpar2i  24381  polid2i  24382  polidi  24383  chdmm2i  24704  chj12i  24748  spanunsni  24805  qlaxr5i  24861  osumcor2i  24870  spansnji  24872  pjadjii  24900  pjinormii  24902  pjsslem  24905  pjpythi  24948  mayete3i  24954  mayete3iOLD  24955  mayetes3i  24956  hoadd12i  25004  honegneg  25033  ho2times  25046  hoaddsubi  25048  hosd1i  25049  hosd2i  25050  honpncani  25054  lnopeq0lem1  25232  lnopunilem1  25237  lnophmlem2  25244  lnfn0i  25269  nmopcoadji  25328  nmopcoadj2i  25329  opsqrlem1  25367  opsqrlem5  25371  opsqrlem6  25372  pjclem3  25424  stadd3i  25475  mddmd2  25536  mdexchi  25562  cvexchlem  25595  atomli  25609  atordi  25611  atabs2i  25629  mdsymlem1  25630  iuninc  25735  archirngz  26030  gsumvsca2  26105  nn0omnd  26163  nn0archi  26165  xrge0slmod  26166  sqsscirc1  26192  cnvordtrestixx  26197  raddcn  26213  xrge0iifhom  26221  xrge0mulc1cn  26225  xrge0tmd  26230  lmlimxrge0  26232  qqhucn  26275  rrhcn  26280  logb1  26316  brfae  26518  cndprobnul  26668  isrrvv  26674  ballotlem1  26717  ballotlem2  26719  ballotlemodife  26728  ballotlemi1  26733  ballotlemii  26734  ballotlemic  26737  ballotlem1c  26738  ballotlemfrceq  26759  ballotth  26768  ofcs2  26794  signsvtn0  26819  signstfveq0  26826  signsvtp  26832  signsvtn  26833  signsvfpn  26834  signsvfnn  26835  signshf  26837  lgamgulmlem2  26864  lgamgulmlem5  26867  lgambdd  26871  subfacp1lem1  26915  subfacp1lem5  26920  subfacp1lem6  26921  subfaclim  26924  cvmliftlem5  27026  cvmliftlem8  27029  cvmliftlem10  27031  cvmliftlem13  27033  cvmlift2lem6  27045  cvmlift2lem12  27051  problem1  27146  problem2  27147  problem4  27149  prodfrec  27257  fprodm1s  27327  fprodp1s  27328  fallfacfwd  27386  0risefac  27388  bpolydiflem  28044  bpoly2  28047  bpoly3  28048  bpoly4  28049  fsumcube  28050  sin2h  28266  mblfinlem3  28274  ismblfin  28276  itg2addnclem3  28289  iblabsnc  28300  iblmulc2nc  28301  itgmulc2nc  28304  ftc1cnnc  28310  ftc1anclem6  28316  ftc1anclem7  28317  ftc1anclem8  28318  dvcnsqr  28322  dvasin  28324  fdc  28485  heiborlem4  28557  heiborlem6  28559  pellexlem5  29019  reglog1  29082  jm2.23  29190  jm2.27c  29201  lnmlsslnm  29279  lmhmlnmsplit  29285  cntzsdrg  29404  areaquad  29437  lhe4.4ex1a  29448  itgsinexplem1  29640  stoweidlem11  29652  stoweidlem13  29654  stoweidlem26  29667  stoweidlem34  29675  wallispilem4  29709  wallispi2lem1  29712  wallispi2lem2  29713  stirlinglem11  29725  modfsummod  30091  numclwwlk5  30551  numclwwlk7  30553  frgraregord013  30557  lincfsuppcl  30656  linccl  30657  lincvalsn  30660  lincdifsn  30667  lincsum  30672  lincscm  30673  lindslinindimp2lem4  30704  lindslinindsimp2lem5  30705  snlindsntor  30714  lincresunit3lem2  30723  zlmodzxzldeplem3  30753  ldepsnlinc  30759  sinh-conventional  30783  onetansqsecsq  30805  cotsqcscsq  30806  dpfrac1  30816  mvlraddi  30826  mvrladdi  30828  mvrraddi  30830  mvlrmuli  30836  sineq0ALT  31375  dalem24  32914  pmod2iN  33066  cdleme9  33470  cdleme20aN  33526  cdleme22e  33561  cdleme22eALTN  33562  cdleme25cv  33575  cdleme29b  33592  cdlemh1  34032  cdlemh2  34033  cdlemk35  34129  cdlemkid1  34139
  Copyright terms: Public domain W3C validator