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

Theorem oveq1i 6200
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 6197 . 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 1370  (class class class)co 6190
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-rex 2801  df-rab 2804  df-v 3070  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-br 4391  df-iota 5479  df-fv 5524  df-ov 6193
This theorem is referenced by:  caov12  6391  caov411  6395  omopthlem1  7194  map1  7488  pw2eng  7517  fsuppunbi  7742  cnfcomlem  8033  cnfcom2  8036  cnfcomlemOLD  8041  cnfcom2OLD  8044  infxpenc2  8289  infxpenc2OLD  8293  adderpqlem  9224  addassnq  9228  distrnq  9231  halfnq  9246  archnq  9250  addclprlem2  9287  addcmpblnr  9340  ltsrpr  9345  m1m1sr  9361  recexsrlem  9371  sqgt0sr  9374  map2psrpr  9378  axi2m1  9427  axcnre  9432  mul02lem2  9647  addid1  9650  cnegex2  9652  addid2  9653  mvlladdi  9728  negsubdi  9766  mulneg1  9882  recextlem1  10067  recdiv  10138  divmul13i  10193  mvllmuli  10265  2p2e4  10540  2times  10541  3p2e5  10555  3p3e6  10556  4p2e6  10557  4p3e7  10558  4p4e8  10559  5p2e7  10560  5p3e8  10561  5p4e9  10562  5p5e10  10563  6p2e8  10564  6p3e9  10565  6p4e10  10566  7p2e9  10567  7p3e10  10568  8p2e10  10569  1mhlfehlf  10645  8th4div3  10646  halfpm6th  10647  nneo  10826  uzindOLD  10837  num0h  10866  numsuc  10868  dec10p  10885  numma  10887  nummac  10888  numma2c  10889  numadd  10890  numaddc  10891  nummul2c  10893  decaddci  10901  decbin0  10959  decbin2  10960  xmulm1  11345  xadddi2  11361  x2times  11363  elfzp1b  11638  elfzm1b  11639  quoremz  11795  quoremnn0ALT  11797  uzrdgxfr  11890  mulexpz  12005  expaddz  12009  sqrecii  12049  cu2  12065  i3  12068  iexpcyc  12071  binom2i  12076  binom2aiOLD  12077  binom3  12086  crreczi  12090  discr  12102  nn0opthlem1  12147  nn0opth2i  12150  faclbnd  12167  bcm1k  12192  bcp1nk  12194  bcpasc  12198  hashp1i  12263  hashxplem  12297  hashpw  12300  hashfun  12301  hashbc  12308  ccatlid  12386  swrdccatin12  12484  revs1  12507  cats1cat  12590  imre  12699  crim  12706  remullem  12719  cnpart  12831  sqrneglem  12858  absexpz  12896  absimle  12900  sqreulem  12949  amgm2  12959  iseraltlem2  13262  iseraltlem3  13263  binomlem  13394  binom11  13397  arisum  13424  arisum2  13425  georeclim  13434  geo2sum  13435  mertenslem1  13446  mertens  13448  efzval  13488  resinval  13521  recosval  13522  efi4p  13523  tan0  13537  efival  13538  sinhval  13540  coshval  13541  cosadd  13551  cos2tsin  13565  ef01bndlem  13570  cos1bnd  13573  cos2bnd  13574  absefib  13584  efieq1re  13585  demoivreALT  13587  eirrlem  13588  rpnnen2lem3  13601  rpnnen2lem11  13609  ruclem7  13620  odd2np1  13694  3dvds  13698  divalglem2  13701  divalglem9  13707  m1bits  13738  sadcp1  13753  sadeq  13770  smupp1  13778  smumul  13791  gcdaddmlem  13814  nn0gcdsq  13932  phiprmpw  13953  prmdiv  13962  prmdiveq  13963  prmdivdiv  13964  pythagtriplem1  13985  pythagtriplem12  13995  pythagtriplem14  13997  pockthi  14070  infpnlem1  14073  prmreclem4  14082  4sqlem12  14119  4sqlem13  14120  4sqlem19  14126  vdwapun  14137  vdwlem6  14149  0hashbc  14170  dec5dvds  14195  dec5nprm  14197  dec2nprm  14198  modxai  14199  modxp1i  14201  mod2xnegi  14202  modsubi  14203  gcdmodi  14205  decexp2  14206  decsplit0b  14211  decsplit1  14213  decsplit  14214  karatsuba  14215  2exp6  14217  2exp8  14218  3exp3  14220  5prm  14238  7prm  14240  11prm  14244  prmlem2  14249  37prm  14250  43prm  14251  83prm  14252  139prm  14253  163prm  14254  317prm  14255  631prm  14256  1259lem1  14257  1259lem2  14258  1259lem3  14259  1259lem4  14260  1259lem5  14261  1259prm  14262  2503lem1  14263  2503lem2  14264  2503lem3  14265  2503prm  14266  4001lem1  14267  4001lem2  14268  4001lem3  14269  4001lem4  14270  4001prm  14271  pwsbas  14527  subsubc  14865  xpccatid  15100  subsubm  15587  mulg2  15738  subsubg  15806  oppgmnd  15971  gsumwrev  15983  psgnunilem2  16103  sylow1lem1  16201  subgslw  16219  sylow3  16236  efginvrel2  16328  efgsfo  16340  frgpnabllem1  16455  gsumzaddlem  16512  gsummptfzsplitl  16531  gsummpt1n0  16561  dprdfid  16612  ablfac1lem  16674  pgpfac1lem3  16683  pgpfaclem1  16687  mgpress  16707  srgbinomlem4  16747  opprrng  16829  unitsubm  16868  subsubrg  16997  lsslss  17148  evlsval  17712  mpff  17726  evl1gsumdlem  17899  gzrngunit  17987  expghm  18032  expghmOLD  18033  chrid  18067  zrhpsgnmhm  18123  psgndiflemA  18140  frlmip  18312  frlmphl  18315  matvsca2  18438  mattposvs  18450  m2detleiblem3  18551  m2detleiblem4  18552  resstopn  18906  cnmpt1res  19365  ressuss  19954  iscusp2  19993  ucnextcn  19995  txmetcnp  20238  rerest  20497  xrtgioo  20499  xrrest  20500  cnmpt2pc  20616  xrhmeo  20634  reust  21001  rrxprds  21009  csbren  21014  minveclem2  21029  ovolunlem1a  21095  ovolicc2lem4  21119  uniioombllem5  21183  iblabs  21422  iblabsr  21423  iblmulc2  21424  itgmulc2  21427  limcres  21477  dvfval  21488  dvreslem  21500  dvres2lem  21501  dvcnp2  21510  cpnres  21527  dvcobr  21536  dveflem  21567  lhop1lem  21601  lhop2  21603  dvcnvrelem2  21606  plyun0  21781  coeeulem  21808  coeeu  21809  dvply1  21866  dvtaylp  21951  taylthlem2  21955  taylth  21956  dvradcnv  22002  pserdvlem2  22009  abelthlem8  22020  abelth  22022  sinhalfpilem  22041  cospi  22050  eulerid  22052  cos2pi  22054  ef2kpi  22056  sinhalfpip  22070  sinhalfpim  22071  coshalfpip  22072  coshalfpim  22073  sincosq3sgn  22078  sincosq4sgn  22079  tangtx  22083  sincos4thpi  22091  sincos6thpi  22093  sineq0  22099  tanregt0  22111  logm1  22153  abslogle  22183  tanarg  22184  logcnlem4  22206  advlogexp  22216  cxpsqr  22264  dvsqr  22298  cxpcn3  22302  root1cj  22310  cxpeq  22311  ang180lem1  22321  ang180lem2  22322  ang180lem3  22323  lawcos  22328  isosctrlem1  22332  isosctrlem2  22333  quad2  22350  1cubrlem  22352  1cubr  22353  dcubic1lem  22354  dcubic2  22355  mcubic  22358  binom4  22361  dquartlem1  22362  quart1lem  22366  quart1  22367  quartlem1  22368  asinlem  22379  asinlem2  22380  asinlem3a  22381  acosneg  22398  efiasin  22399  asinsinlem  22402  asinsin  22403  acoscos  22404  asin1  22405  acosbnd  22411  atancj  22421  efiatan  22423  atanlogaddlem  22424  efiatan2  22428  2efiatan  22429  tanatan  22430  cosatan  22432  atantan  22434  atanbndlem  22436  atans2  22442  dvatan  22446  atantayl  22448  atantayl2  22449  log2cnv  22455  log2tlbnd  22456  log2ublem2  22458  log2ublem3  22459  log2ub  22460  birthday  22464  jensenlem1  22496  amgmlem  22499  wilthlem1  22522  ftalem2  22527  ftalem5  22530  ftalem6  22531  basellem2  22535  basellem3  22536  basellem5  22538  basellem8  22541  basellem9  22542  mule1  22602  ppi1i  22622  musum  22647  ppiublem1  22657  ppiublem2  22658  ppiub  22659  chtublem  22666  chtub  22667  dchrptlem1  22719  dchrptlem2  22720  bclbnd  22735  bpos1  22738  bposlem6  22744  bposlem8  22746  bposlem9  22747  lgslem4  22754  lgsdir2lem1  22778  lgsdir2lem2  22779  lgsdir2lem4  22781  lgsdir2lem5  22782  lgsne0  22788  1lgs  22792  lgseisenlem1  22804  lgseisenlem2  22805  lgseisenlem3  22806  lgseisenlem4  22807  lgseisen  22808  lgsquadlem1  22809  lgsquadlem2  22810  lgsquad2lem1  22813  lgsquad2lem2  22814  m1lgs  22817  chebbnd1lem2  22835  chebbnd1lem3  22836  rplogsumlem2  22850  dchrisum0flblem1  22873  dchrisum0re  22878  mulog2sumlem2  22900  chpdifbndlem1  22918  pntpbnd1a  22950  pntpbnd2  22952  pntibndlem2  22956  pntibndlem3  22957  pntlemg  22963  pntlemk  22971  pntlemo  22972  axsegconlem1  23298  ax5seglem7  23316  axlowdimlem3  23325  axlowdimlem16  23338  axlowdimlem17  23339  usgraexvlem  23448  fargshiftlem  23655  constr3trllem3  23673  eupares  23731  konigsberg  23743  ex-fl  23789  addinv  23974  vc2  24068  vc0  24082  vcm  24084  vcnegneg  24087  nvnncan  24178  nvm1  24187  nvpi  24189  nvmtri  24194  nvge0  24197  ipval3  24239  ipidsq  24243  ip0i  24360  ip1ilem  24361  ip2i  24363  ipdirilem  24364  ipasslem10  24374  siilem1  24386  siii  24388  minvecolem2  24411  hvsubid  24563  hvaddsubval  24570  hvmul2negi  24585  hvadd12i  24594  hv2times  24598  hvnegdii  24599  hvaddcani  24602  hi01  24633  hisubcomi  24641  normlem0  24646  normlem1  24647  normlem3  24649  normlem9  24655  bcseqi  24657  normsqi  24669  norm-ii-i  24674  normsubi  24678  norm3difi  24684  norm3adifii  24685  normpar2i  24693  polid2i  24694  polidi  24695  chdmm2i  25016  chj12i  25060  spanunsni  25117  qlaxr5i  25173  osumcor2i  25182  spansnji  25184  pjadjii  25212  pjinormii  25214  pjsslem  25217  pjpythi  25260  mayete3i  25266  mayete3iOLD  25267  mayetes3i  25268  hoadd12i  25316  honegneg  25345  ho2times  25358  hoaddsubi  25360  hosd1i  25361  hosd2i  25362  honpncani  25366  lnopeq0lem1  25544  lnopunilem1  25549  lnophmlem2  25556  lnfn0i  25581  nmopcoadji  25640  nmopcoadj2i  25641  opsqrlem1  25679  opsqrlem5  25683  opsqrlem6  25684  pjclem3  25736  stadd3i  25787  mddmd2  25848  mdexchi  25874  cvexchlem  25907  atomli  25921  atordi  25923  atabs2i  25941  mdsymlem1  25942  iuninc  26045  suppss3  26161  archirngz  26340  gsumvsca2  26386  nn0omnd  26443  nn0archi  26445  xrge0slmod  26446  sqsscirc1  26472  cnvordtrestixx  26477  raddcn  26493  xrge0iifhom  26501  xrge0mulc1cn  26505  xrge0tmd  26510  lmlimxrge0  26512  qqhucn  26555  rrhcn  26560  logb1  26596  brfae  26798  cndprobnul  26954  isrrvv  26960  ballotlem1  27003  ballotlem2  27005  ballotlemodife  27014  ballotlemi1  27019  ballotlemii  27020  ballotlemic  27023  ballotlem1c  27024  ballotlemfrceq  27045  ballotth  27054  ofcs2  27080  signsvtn0  27105  signstfveq0  27112  signsvtp  27118  signsvtn  27119  signsvfpn  27120  signsvfnn  27121  signshf  27123  lgamgulmlem2  27150  lgamgulmlem5  27153  lgambdd  27157  subfacp1lem1  27201  subfacp1lem5  27206  subfacp1lem6  27207  subfaclim  27210  cvmliftlem5  27312  cvmliftlem8  27315  cvmliftlem10  27317  cvmliftlem13  27319  cvmlift2lem6  27331  cvmlift2lem12  27337  problem1  27432  problem2  27433  problem4  27435  quad3  27437  prodfrec  27544  fprodm1s  27614  fprodp1s  27615  fallfacfwd  27673  0risefac  27675  bpolydiflem  28331  bpoly2  28334  bpoly3  28335  bpoly4  28336  fsumcube  28337  sin2h  28560  mblfinlem3  28568  ismblfin  28570  itg2addnclem3  28583  iblabsnc  28594  iblmulc2nc  28595  itgmulc2nc  28598  ftc1cnnc  28604  ftc1anclem6  28610  ftc1anclem7  28611  ftc1anclem8  28612  dvcnsqr  28616  dvasin  28618  fdc  28779  heiborlem4  28851  heiborlem6  28853  pellexlem5  29312  reglog1  29375  jm2.23  29483  jm2.27c  29494  lnmlsslnm  29572  lmhmlnmsplit  29578  cntzsdrg  29697  areaquad  29730  lhe4.4ex1a  29741  itgsinexplem1  29932  stoweidlem11  29944  stoweidlem13  29946  stoweidlem26  29959  stoweidlem34  29967  wallispilem4  30001  wallispi2lem1  30004  wallispi2lem2  30005  stirlinglem11  30017  modfsummod  30383  numclwwlk5  30843  numclwwlk7  30845  frgraregord013  30849  altgsumbcALT  30888  coe1fzgsumdlem  30979  lincfsuppcl  31054  linccl  31055  lincvalsn  31058  lincdifsn  31065  lincsum  31070  lincscm  31071  lindslinindimp2lem4  31102  lindslinindsimp2lem5  31103  snlindsntor  31112  lincresunit3lem2  31121  zlmodzxzldeplem3  31151  ldepsnlinc  31157  cpmidpmat  31327  sinh-conventional  31370  onetansqsecsq  31392  cotsqcscsq  31393  dpfrac1  31403  mvlraddi  31417  mvrladdi  31419  mvrraddi  31421  mvlrmuli  31429  sineq0ALT  31973  dalem24  33647  pmod2iN  33799  cdleme9  34203  cdleme20aN  34259  cdleme22e  34294  cdleme22eALTN  34295  cdleme25cv  34308  cdleme29b  34325  cdlemh1  34765  cdlemh2  34766  cdlemk35  34862  cdlemkid1  34872
  Copyright terms: Public domain W3C validator