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

Theorem oveq1i 6096
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 6093 . 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 1369  (class class class)co 6086
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-iota 5376  df-fv 5421  df-ov 6089
This theorem is referenced by:  caov12  6286  caov411  6290  omopthlem1  7086  map1  7380  pw2eng  7409  fsuppunbi  7633  cnfcomlem  7924  cnfcom2  7927  cnfcomlemOLD  7932  cnfcom2OLD  7935  infxpenc2  8180  infxpenc2OLD  8184  adderpqlem  9115  addassnq  9119  distrnq  9122  halfnq  9137  archnq  9141  addclprlem2  9178  addcmpblnr  9231  ltsrpr  9236  m1m1sr  9252  recexsrlem  9262  sqgt0sr  9265  map2psrpr  9269  axi2m1  9318  axcnre  9323  mul02lem2  9538  addid1  9541  cnegex2  9543  addid2  9544  mvlladdi  9619  negsubdi  9657  mulneg1  9773  recextlem1  9958  recdiv  10029  divmul13i  10084  mvllmuli  10156  2p2e4  10431  2times  10432  3p2e5  10446  3p3e6  10447  4p2e6  10448  4p3e7  10449  4p4e8  10450  5p2e7  10451  5p3e8  10452  5p4e9  10453  5p5e10  10454  6p2e8  10455  6p3e9  10456  6p4e10  10457  7p2e9  10458  7p3e10  10459  8p2e10  10460  1mhlfehlf  10536  8th4div3  10537  halfpm6th  10538  nneo  10717  uzindOLD  10728  num0h  10757  numsuc  10759  dec10p  10776  numma  10778  nummac  10779  numma2c  10780  numadd  10781  numaddc  10782  nummul2c  10784  decaddci  10792  decbin0  10850  decbin2  10851  xmulm1  11236  xadddi2  11252  x2times  11254  elfzp1b  11529  elfzm1b  11530  quoremz  11686  quoremnn0ALT  11688  uzrdgxfr  11781  mulexpz  11896  expaddz  11900  sqrecii  11940  cu2  11956  i3  11959  iexpcyc  11962  binom2i  11967  binom2aiOLD  11968  binom3  11977  crreczi  11981  discr  11993  nn0opthlem1  12038  nn0opth2i  12041  faclbnd  12058  bcm1k  12083  bcp1nk  12085  bcpasc  12089  hashp1i  12153  hashxplem  12187  hashpw  12190  hashfun  12191  hashbc  12198  ccatlid  12276  swrdccatin12  12374  revs1  12397  cats1cat  12480  imre  12589  crim  12596  remullem  12609  cnpart  12721  sqrneglem  12748  absexpz  12786  absimle  12790  sqreulem  12839  amgm2  12849  iseraltlem2  13152  iseraltlem3  13153  binomlem  13284  binom11  13287  arisum  13314  arisum2  13315  georeclim  13324  geo2sum  13325  mertenslem1  13336  mertens  13338  efzval  13378  resinval  13411  recosval  13412  efi4p  13413  tan0  13427  efival  13428  sinhval  13430  coshval  13431  cosadd  13441  cos2tsin  13455  ef01bndlem  13460  cos1bnd  13463  cos2bnd  13464  absefib  13474  efieq1re  13475  demoivreALT  13477  eirrlem  13478  rpnnen2lem3  13491  rpnnen2lem11  13499  ruclem7  13510  odd2np1  13584  3dvds  13588  divalglem2  13591  divalglem9  13597  m1bits  13628  sadcp1  13643  sadeq  13660  smupp1  13668  smumul  13681  gcdaddmlem  13704  nn0gcdsq  13822  phiprmpw  13843  prmdiv  13852  prmdiveq  13853  prmdivdiv  13854  pythagtriplem1  13875  pythagtriplem12  13885  pythagtriplem14  13887  pockthi  13960  infpnlem1  13963  prmreclem4  13972  4sqlem12  14009  4sqlem13  14010  4sqlem19  14016  vdwapun  14027  vdwlem6  14039  0hashbc  14060  dec5dvds  14085  dec5nprm  14087  dec2nprm  14088  modxai  14089  modxp1i  14091  mod2xnegi  14092  modsubi  14093  gcdmodi  14095  decexp2  14096  decsplit0b  14101  decsplit1  14103  decsplit  14104  karatsuba  14105  2exp6  14107  2exp8  14108  3exp3  14110  5prm  14128  7prm  14130  11prm  14134  prmlem2  14139  37prm  14140  43prm  14141  83prm  14142  139prm  14143  163prm  14144  317prm  14145  631prm  14146  1259lem1  14147  1259lem2  14148  1259lem3  14149  1259lem4  14150  1259lem5  14151  1259prm  14152  2503lem1  14153  2503lem2  14154  2503lem3  14155  2503prm  14156  4001lem1  14157  4001lem2  14158  4001lem3  14159  4001lem4  14160  4001prm  14161  pwsbas  14417  subsubc  14755  xpccatid  14990  subsubm  15476  mulg2  15627  subsubg  15695  oppgmnd  15860  gsumwrev  15872  psgnunilem2  15992  sylow1lem1  16088  subgslw  16106  sylow3  16123  efginvrel2  16215  efgsfo  16227  frgpnabllem1  16342  gsumzaddlem  16399  gsummptif1n0  16445  dprdfid  16495  ablfac1lem  16557  pgpfac1lem3  16566  pgpfaclem1  16570  mgpress  16590  srgbinomlem4  16629  opprrng  16711  unitsubm  16750  subsubrg  16869  lsslss  17019  evlsval  17580  mpff  17594  evl1gsumdlem  17765  gzrngunit  17853  expghm  17898  expghmOLD  17899  chrid  17933  zrhpsgnmhm  17989  psgndiflemA  18006  frlmip  18178  frlmphl  18181  matvsca2  18303  mattposvs  18314  m2detleiblem3  18410  m2detleiblem4  18411  resstopn  18765  cnmpt1res  19224  ressuss  19813  iscusp2  19852  ucnextcn  19854  txmetcnp  20097  rerest  20356  xrtgioo  20358  xrrest  20359  cnmpt2pc  20475  xrhmeo  20493  reust  20860  rrxprds  20868  csbren  20873  minveclem2  20888  ovolunlem1a  20954  ovolicc2lem4  20978  uniioombllem5  21042  iblabs  21281  iblabsr  21282  iblmulc2  21283  itgmulc2  21286  limcres  21336  dvfval  21347  dvreslem  21359  dvres2lem  21360  dvcnp2  21369  cpnres  21386  dvcobr  21395  dveflem  21426  lhop1lem  21460  lhop2  21462  dvcnvrelem2  21465  plyun0  21640  coeeulem  21667  coeeu  21668  dvply1  21725  dvtaylp  21810  taylthlem2  21814  taylth  21815  dvradcnv  21861  pserdvlem2  21868  abelthlem8  21879  abelth  21881  sinhalfpilem  21900  cospi  21909  eulerid  21911  cos2pi  21913  ef2kpi  21915  sinhalfpip  21929  sinhalfpim  21930  coshalfpip  21931  coshalfpim  21932  sincosq3sgn  21937  sincosq4sgn  21938  tangtx  21942  sincos4thpi  21950  sincos6thpi  21952  sineq0  21958  tanregt0  21970  logm1  22012  abslogle  22042  tanarg  22043  logcnlem4  22065  advlogexp  22075  cxpsqr  22123  dvsqr  22157  cxpcn3  22161  root1cj  22169  cxpeq  22170  ang180lem1  22180  ang180lem2  22181  ang180lem3  22182  lawcos  22187  isosctrlem1  22191  isosctrlem2  22192  quad2  22209  1cubrlem  22211  1cubr  22212  dcubic1lem  22213  dcubic2  22214  mcubic  22217  binom4  22220  dquartlem1  22221  quart1lem  22225  quart1  22226  quartlem1  22227  asinlem  22238  asinlem2  22239  asinlem3a  22240  acosneg  22257  efiasin  22258  asinsinlem  22261  asinsin  22262  acoscos  22263  asin1  22264  acosbnd  22270  atancj  22280  efiatan  22282  atanlogaddlem  22283  efiatan2  22287  2efiatan  22288  tanatan  22289  cosatan  22291  atantan  22293  atanbndlem  22295  atans2  22301  dvatan  22305  atantayl  22307  atantayl2  22308  log2cnv  22314  log2tlbnd  22315  log2ublem2  22317  log2ublem3  22318  log2ub  22319  birthday  22323  jensenlem1  22355  amgmlem  22358  wilthlem1  22381  ftalem2  22386  ftalem5  22389  ftalem6  22390  basellem2  22394  basellem3  22395  basellem5  22397  basellem8  22400  basellem9  22401  mule1  22461  ppi1i  22481  musum  22506  ppiublem1  22516  ppiublem2  22517  ppiub  22518  chtublem  22525  chtub  22526  dchrptlem1  22578  dchrptlem2  22579  bclbnd  22594  bpos1  22597  bposlem6  22603  bposlem8  22605  bposlem9  22606  lgslem4  22613  lgsdir2lem1  22637  lgsdir2lem2  22638  lgsdir2lem4  22640  lgsdir2lem5  22641  lgsne0  22647  1lgs  22651  lgseisenlem1  22663  lgseisenlem2  22664  lgseisenlem3  22665  lgseisenlem4  22666  lgseisen  22667  lgsquadlem1  22668  lgsquadlem2  22669  lgsquad2lem1  22672  lgsquad2lem2  22673  m1lgs  22676  chebbnd1lem2  22694  chebbnd1lem3  22695  rplogsumlem2  22709  dchrisum0flblem1  22732  dchrisum0re  22737  mulog2sumlem2  22759  chpdifbndlem1  22777  pntpbnd1a  22809  pntpbnd2  22811  pntibndlem2  22815  pntibndlem3  22816  pntlemg  22822  pntlemk  22830  pntlemo  22831  axsegconlem1  23114  ax5seglem7  23132  axlowdimlem3  23141  axlowdimlem16  23154  axlowdimlem17  23155  usgraexvlem  23264  fargshiftlem  23471  constr3trllem3  23489  eupares  23547  konigsberg  23559  ex-fl  23605  addinv  23790  vc2  23884  vc0  23898  vcm  23900  vcnegneg  23903  nvnncan  23994  nvm1  24003  nvpi  24005  nvmtri  24010  nvge0  24013  ipval3  24055  ipidsq  24059  ip0i  24176  ip1ilem  24177  ip2i  24179  ipdirilem  24180  ipasslem10  24190  siilem1  24202  siii  24204  minvecolem2  24227  hvsubid  24379  hvaddsubval  24386  hvmul2negi  24401  hvadd12i  24410  hv2times  24414  hvnegdii  24415  hvaddcani  24418  hi01  24449  hisubcomi  24457  normlem0  24462  normlem1  24463  normlem3  24465  normlem9  24471  bcseqi  24473  normsqi  24485  norm-ii-i  24490  normsubi  24494  norm3difi  24500  norm3adifii  24501  normpar2i  24509  polid2i  24510  polidi  24511  chdmm2i  24832  chj12i  24876  spanunsni  24933  qlaxr5i  24989  osumcor2i  24998  spansnji  25000  pjadjii  25028  pjinormii  25030  pjsslem  25033  pjpythi  25076  mayete3i  25082  mayete3iOLD  25083  mayetes3i  25084  hoadd12i  25132  honegneg  25161  ho2times  25174  hoaddsubi  25176  hosd1i  25177  hosd2i  25178  honpncani  25182  lnopeq0lem1  25360  lnopunilem1  25365  lnophmlem2  25372  lnfn0i  25397  nmopcoadji  25456  nmopcoadj2i  25457  opsqrlem1  25495  opsqrlem5  25499  opsqrlem6  25500  pjclem3  25552  stadd3i  25603  mddmd2  25664  mdexchi  25690  cvexchlem  25723  atomli  25737  atordi  25739  atabs2i  25757  mdsymlem1  25758  iuninc  25862  suppss3  25978  archirngz  26157  gsumvsca2  26203  nn0omnd  26261  nn0archi  26263  xrge0slmod  26264  sqsscirc1  26290  cnvordtrestixx  26295  raddcn  26311  xrge0iifhom  26319  xrge0mulc1cn  26323  xrge0tmd  26328  lmlimxrge0  26330  qqhucn  26373  rrhcn  26378  logb1  26414  brfae  26616  cndprobnul  26772  isrrvv  26778  ballotlem1  26821  ballotlem2  26823  ballotlemodife  26832  ballotlemi1  26837  ballotlemii  26838  ballotlemic  26841  ballotlem1c  26842  ballotlemfrceq  26863  ballotth  26872  ofcs2  26898  signsvtn0  26923  signstfveq0  26930  signsvtp  26936  signsvtn  26937  signsvfpn  26938  signsvfnn  26939  signshf  26941  lgamgulmlem2  26968  lgamgulmlem5  26971  lgambdd  26975  subfacp1lem1  27019  subfacp1lem5  27024  subfacp1lem6  27025  subfaclim  27028  cvmliftlem5  27130  cvmliftlem8  27133  cvmliftlem10  27135  cvmliftlem13  27137  cvmlift2lem6  27149  cvmlift2lem12  27155  problem1  27250  problem2  27251  problem4  27253  prodfrec  27361  fprodm1s  27431  fprodp1s  27432  fallfacfwd  27490  0risefac  27492  bpolydiflem  28148  bpoly2  28151  bpoly3  28152  bpoly4  28153  fsumcube  28154  sin2h  28375  mblfinlem3  28383  ismblfin  28385  itg2addnclem3  28398  iblabsnc  28409  iblmulc2nc  28410  itgmulc2nc  28413  ftc1cnnc  28419  ftc1anclem6  28425  ftc1anclem7  28426  ftc1anclem8  28427  dvcnsqr  28431  dvasin  28433  fdc  28594  heiborlem4  28666  heiborlem6  28668  pellexlem5  29127  reglog1  29190  jm2.23  29298  jm2.27c  29309  lnmlsslnm  29387  lmhmlnmsplit  29393  cntzsdrg  29512  areaquad  29545  lhe4.4ex1a  29556  itgsinexplem1  29747  stoweidlem11  29759  stoweidlem13  29761  stoweidlem26  29774  stoweidlem34  29782  wallispilem4  29816  wallispi2lem1  29819  wallispi2lem2  29820  stirlinglem11  29832  modfsummod  30198  numclwwlk5  30658  numclwwlk7  30660  frgraregord013  30664  altgsumbcALT  30701  lincfsuppcl  30836  linccl  30837  lincvalsn  30840  lincdifsn  30847  lincsum  30852  lincscm  30853  lindslinindimp2lem4  30884  lindslinindsimp2lem5  30885  snlindsntor  30894  lincresunit3lem2  30903  zlmodzxzldeplem3  30933  ldepsnlinc  30939  sinh-conventional  30963  onetansqsecsq  30985  cotsqcscsq  30986  dpfrac1  30996  mvlraddi  31006  mvrladdi  31008  mvrraddi  31010  mvlrmuli  31016  sineq0ALT  31560  dalem24  33181  pmod2iN  33333  cdleme9  33737  cdleme20aN  33793  cdleme22e  33828  cdleme22eALTN  33829  cdleme25cv  33842  cdleme29b  33859  cdlemh1  34299  cdlemh2  34300  cdlemk35  34396  cdlemkid1  34406
  Copyright terms: Public domain W3C validator