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

Theorem oveq1i 6093
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 6090 . 2  |-  ( A  =  B  ->  ( A F C )  =  ( B F C ) )
31, 2ax-mp 8 1  |-  ( A F C )  =  ( B F C )
Colors of variables: wff set class
Syntax hints:    = wceq 1653  (class class class)co 6083
This theorem is referenced by:  caov12  6277  caov411  6281  omopthlem1  6900  map1  7187  pw2eng  7216  cnfcomlem  7658  cnfcom2  7661  infxpenc2  7905  adderpqlem  8833  addassnq  8837  distrnq  8840  halfnq  8855  archnq  8859  addclprlem2  8896  addcmpblnr  8949  ltsrpr  8954  m1m1sr  8970  recexsrlem  8980  sqgt0sr  8983  map2psrpr  8987  axi2m1  9036  axcnre  9041  mul02lem2  9245  addid1  9248  cnegex2  9250  addid2  9251  negsubdi  9359  mulneg1  9472  recextlem1  9654  recdiv  9722  divmul13i  9777  2p2e4  10100  2times  10101  3p2e5  10113  3p3e6  10114  4p2e6  10115  4p3e7  10116  4p4e8  10117  5p2e7  10118  5p3e8  10119  5p4e9  10120  5p5e10  10121  6p2e8  10122  6p3e9  10123  6p4e10  10124  7p2e9  10125  7p3e10  10126  8p2e10  10127  1mhlfehlf  10192  8th4div3  10193  halfpm6th  10194  nneo  10355  uzindOLD  10366  num0h  10394  numsuc  10396  dec10p  10413  numma  10415  nummac  10416  numma2c  10417  numadd  10418  numaddc  10419  nummul2c  10421  decaddci  10429  decbin0  10487  decbin2  10488  xmulm1  10862  xadddi2  10878  x2times  10880  elfzm1b  11127  quoremz  11238  quoremnn0ALT  11240  uzrdgxfr  11308  mulexpz  11422  expaddz  11426  sqrecii  11466  cu2  11481  i3  11484  iexpcyc  11487  binom2i  11492  binom2aiOLD  11493  binom3  11502  crreczi  11506  discr  11518  nn0opthlem1  11563  nn0opth2i  11566  faclbnd  11583  bcm1k  11608  bcp1nk  11610  bcpasc  11614  hashp1i  11674  hashxplem  11698  hashpw  11701  hashfun  11702  hashbc  11704  ccatlid  11750  revs1  11799  cats1cat  11827  imre  11915  crim  11922  remullem  11935  cnpart  12047  sqrneglem  12074  absexpz  12112  absimle  12116  sqreulem  12165  amgm2  12175  iseraltlem2  12478  iseraltlem3  12479  binomlem  12610  binom11  12613  arisum  12641  arisum2  12642  georeclim  12651  geo2sum  12652  mertenslem1  12663  mertens  12665  efzval  12705  resinval  12738  recosval  12739  efi4p  12740  tan0  12754  efival  12755  sinhval  12757  coshval  12758  cosadd  12768  cos2tsin  12782  ef01bndlem  12787  cos1bnd  12790  cos2bnd  12791  absefib  12801  efieq1re  12802  demoivreALT  12804  eirrlem  12805  rpnnen2lem3  12818  rpnnen2lem11  12826  ruclem7  12837  odd2np1  12910  3dvds  12914  divalglem2  12917  divalglem9  12923  m1bits  12954  sadcp1  12969  sadeq  12986  smupp1  12994  smumul  13007  gcdaddmlem  13030  nn0gcdsq  13146  phiprmpw  13167  prmdiv  13176  prmdiveq  13177  prmdivdiv  13178  pythagtriplem1  13192  pythagtriplem12  13202  pythagtriplem14  13204  pockthi  13277  infpnlem1  13280  prmreclem4  13289  4sqlem12  13326  4sqlem13  13327  4sqlem19  13333  vdwapun  13344  vdwlem6  13356  0hashbc  13377  dec5dvds  13402  dec5nprm  13404  dec2nprm  13405  modxai  13406  modxp1i  13408  mod2xnegi  13409  modsubi  13410  gcdmodi  13412  decexp2  13413  decsplit0b  13418  decsplit1  13420  decsplit  13421  karatsuba  13422  2exp6  13424  2exp8  13425  3exp3  13427  5prm  13433  7prm  13435  11prm  13439  prmlem2  13444  37prm  13445  43prm  13446  83prm  13447  139prm  13448  163prm  13449  317prm  13450  631prm  13451  1259lem1  13452  1259lem2  13453  1259lem3  13454  1259lem4  13455  1259lem5  13456  1259prm  13457  2503lem1  13458  2503lem2  13459  2503lem3  13460  2503prm  13461  4001lem1  13462  4001lem2  13463  4001lem3  13464  4001lem4  13465  4001prm  13466  pwsbas  13711  subsubc  14052  xpccatid  14287  subsubm  14759  mulg2  14901  subsubg  14965  oppgmnd  15152  gsumwrev  15164  sylow1lem1  15234  subgslw  15252  sylow3  15269  efginvrel2  15361  efgsfo  15373  frgpnabllem1  15486  ablfac1lem  15628  pgpfac1lem3  15637  pgpfaclem1  15641  mgpress  15661  opprrng  15738  unitsubm  15777  subsubrg  15896  lsslss  16039  gzrngunit  16766  expghm  16779  zrhval  16791  chrid  16810  resstopn  17252  cnmpt1res  17710  ressuss  18295  iscusp2  18334  ucnextcn  18336  txmetcnp  18579  rerest  18837  xrtgioo  18839  xrrest  18840  cnmpt2pc  18955  xrhmeo  18973  minveclem2  19329  ovolunlem1a  19394  ovolicc2lem4  19418  uniioombllem5  19481  iblabs  19722  iblabsr  19723  iblmulc2  19724  itgmulc2  19727  limcres  19775  dvfval  19786  dvreslem  19798  dvres2lem  19799  dvcnp2  19808  cpnres  19825  dvcobr  19834  dveflem  19865  lhop1lem  19899  lhop2  19901  dvcnvrelem2  19904  evlsval  19942  mpff  19964  plyun0  20118  coeeulem  20145  coeeu  20146  dvply1  20203  dvtaylp  20288  taylthlem2  20292  taylth  20293  dvradcnv  20339  pserdvlem2  20346  abelthlem8  20357  abelth  20359  sinhalfpilem  20376  cospi  20382  eulerid  20384  cos2pi  20386  ef2kpi  20388  sinhalfpip  20402  sinhalfpim  20403  coshalfpip  20404  coshalfpim  20405  sincosq3sgn  20410  sincosq4sgn  20411  tangtx  20415  sincos4thpi  20423  sincos6thpi  20425  sineq0  20431  tanregt0  20443  logm1  20485  abslogle  20515  tanarg  20516  logcnlem4  20538  advlogexp  20548  cxpsqr  20596  dvsqr  20630  cxpcn3  20634  root1cj  20642  cxpeq  20643  ang180lem1  20653  ang180lem2  20654  ang180lem3  20655  lawcos  20660  isosctrlem1  20664  isosctrlem2  20665  quad2  20681  1cubrlem  20683  1cubr  20684  dcubic1lem  20685  dcubic2  20686  mcubic  20689  binom4  20692  dquartlem1  20693  quart1lem  20697  quart1  20698  quartlem1  20699  asinlem  20710  asinlem2  20711  asinlem3a  20712  acosneg  20729  efiasin  20730  asinsinlem  20733  asinsin  20734  acoscos  20735  asin1  20736  acosbnd  20742  atancj  20752  efiatan  20754  atanlogaddlem  20755  efiatan2  20759  2efiatan  20760  tanatan  20761  cosatan  20763  atantan  20765  atanbndlem  20767  atans2  20773  dvatan  20777  atantayl  20779  atantayl2  20780  log2cnv  20786  log2tlbnd  20787  log2ublem2  20789  log2ublem3  20790  log2ub  20791  birthday  20795  jensenlem1  20827  amgmlem  20830  wilthlem1  20853  ftalem2  20858  ftalem5  20861  ftalem6  20862  basellem2  20866  basellem3  20867  basellem5  20869  basellem8  20872  basellem9  20873  mule1  20933  ppi1i  20953  musum  20978  ppiublem1  20988  ppiublem2  20989  ppiub  20990  chtublem  20997  chtub  20998  dchrptlem1  21050  dchrptlem2  21051  bclbnd  21066  bpos1  21069  bposlem6  21075  bposlem8  21077  bposlem9  21078  lgslem4  21085  lgsdir2lem1  21109  lgsdir2lem2  21110  lgsdir2lem4  21112  lgsdir2lem5  21113  lgsne0  21119  1lgs  21123  lgseisenlem1  21135  lgseisenlem2  21136  lgseisenlem3  21137  lgseisenlem4  21138  lgseisen  21139  lgsquadlem1  21140  lgsquadlem2  21141  lgsquad2lem1  21144  lgsquad2lem2  21145  m1lgs  21148  chebbnd1lem2  21166  chebbnd1lem3  21167  rplogsumlem2  21181  dchrisum0flblem1  21204  dchrisum0re  21209  mulog2sumlem2  21231  chpdifbndlem1  21249  pntpbnd1a  21281  pntpbnd2  21283  pntibndlem2  21287  pntibndlem3  21288  pntlemg  21294  pntlemk  21302  pntlemo  21303  usgraexvlem  21416  fargshiftlem  21623  constr3trllem3  21641  eupares  21699  konigsberg  21711  ex-fl  21757  addinv  21942  vc2  22036  vc0  22050  vcm  22052  vcnegneg  22055  nvnncan  22146  nvm1  22155  nvpi  22157  nvmtri  22162  nvge0  22165  ipval3  22207  ipidsq  22211  ip0i  22328  ip1ilem  22329  ip2i  22331  ipdirilem  22332  ipasslem10  22342  siilem1  22354  siii  22356  minvecolem2  22379  hvsubid  22530  hvaddsubval  22537  hvmul2negi  22552  hvadd12i  22561  hv2times  22565  hvnegdii  22566  hvaddcani  22569  hi01  22600  hisubcomi  22608  normlem0  22613  normlem1  22614  normlem3  22616  normlem9  22622  bcseqi  22624  normsqi  22636  norm-ii-i  22641  normsubi  22645  norm3difi  22651  norm3adifii  22652  normpar2i  22660  polid2i  22661  polidi  22662  chdmm2i  22982  chj12i  23026  spanunsni  23083  qlaxr5i  23139  osumcor2i  23148  spansnji  23150  pjadjii  23178  pjinormii  23180  pjsslem  23183  pjpythi  23226  mayete3i  23232  mayete3iOLD  23233  mayetes3i  23234  hoadd12i  23282  honegneg  23311  ho2times  23324  hoaddsubi  23326  hosd1i  23327  hosd2i  23328  honpncani  23332  lnopeq0lem1  23510  lnopunilem1  23515  lnophmlem2  23522  lnfn0i  23547  nmopcoadji  23606  nmopcoadj2i  23607  opsqrlem1  23645  opsqrlem5  23649  opsqrlem6  23650  pjclem3  23702  stadd3i  23753  mddmd2  23814  mdexchi  23840  cvexchlem  23873  atomli  23887  atordi  23889  atabs2i  23907  mdsymlem1  23908  iuninc  24013  sqsscirc1  24308  cnvordtrestixx  24313  raddcn  24317  xrge0iifhom  24325  xrge0mulc1cn  24329  xrge0tmd  24334  lmlimxrge0  24336  reust  24346  qqhucn  24378  rrhre  24389  logb1  24405  brfae  24601  cndprobnul  24697  isrrvv  24703  ballotlem1  24746  ballotlem2  24748  ballotlemodife  24757  ballotlemi1  24762  ballotlemii  24763  ballotlemic  24766  ballotlem1c  24767  ballotlemfrceq  24788  ballotth  24797  lgamgulmlem2  24816  lgamgulmlem5  24819  lgambdd  24823  subfacp1lem1  24867  subfacp1lem5  24872  subfacp1lem6  24873  subfaclim  24876  cvmliftlem5  24978  cvmliftlem8  24981  cvmliftlem10  24983  cvmliftlem13  24985  cvmlift2lem6  24997  cvmlift2lem12  25003  elfzp1b  25118  prodfrec  25225  fprodm1s  25295  fprodp1s  25296  fallfacfwd  25354  0risefac  25356  axsegconlem1  25858  ax5seglem7  25876  axlowdimlem3  25885  axlowdimlem16  25898  axlowdimlem17  25899  bpolydiflem  26102  bpoly2  26105  bpoly3  26106  bpoly4  26107  fsumcube  26108  mblfinlem3  26247  ismblfin  26249  itg2addnclem3  26260  iblabsnc  26271  iblmulc2nc  26272  itgmulc2nc  26275  ftc1cnnc  26281  ftc1anclem6  26287  ftc1anclem7  26288  ftc1anclem8  26289  fdc  26451  csbrn  26458  heiborlem4  26525  heiborlem6  26527  pellexlem5  26898  reglog1  26961  jm2.23  27069  jm2.27c  27080  lnmlsslnm  27158  lmhmlnmsplit  27164  psgnunilem2  27397  matvsca2  27457  cntzsdrg  27489  lhe4.4ex1a  27525  itgsinexplem1  27726  stoweidlem11  27738  stoweidlem13  27740  stoweidlem26  27753  stoweidlem34  27761  wallispilem4  27795  wallispi2lem1  27798  wallispi2lem2  27799  stirlinglem11  27811  swrdccatin12  28216  sinh-conventional  28484  onetansqsecsq  28506  cotsqcscsq  28507  dpfrac1  28517  sineq0ALT  29051  dalem24  30496  pmod2iN  30648  cdleme9  31052  cdleme20aN  31108  cdleme22e  31143  cdleme22eALTN  31144  cdleme25cv  31157  cdleme29b  31174  cdlemh1  31614  cdlemh2  31615  cdlemk35  31711  cdlemkid1  31721
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rex 2713  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4215  df-iota 5420  df-fv 5464  df-ov 6086
  Copyright terms: Public domain W3C validator