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

Theorem oveq1i 6050
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 6047 . 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 1649  (class class class)co 6040
This theorem is referenced by:  caov12  6234  caov411  6238  omopthlem1  6857  map1  7144  pw2eng  7173  cnfcomlem  7612  cnfcom2  7615  infxpenc2  7859  adderpqlem  8787  addassnq  8791  distrnq  8794  halfnq  8809  archnq  8813  addclprlem2  8850  addcmpblnr  8903  ltsrpr  8908  m1m1sr  8924  recexsrlem  8934  sqgt0sr  8937  map2psrpr  8941  axi2m1  8990  axcnre  8995  mul02lem2  9199  addid1  9202  cnegex2  9204  addid2  9205  negsubdi  9313  mulneg1  9426  recextlem1  9608  recdiv  9676  divmul13i  9731  2p2e4  10054  2times  10055  3p2e5  10067  3p3e6  10068  4p2e6  10069  4p3e7  10070  4p4e8  10071  5p2e7  10072  5p3e8  10073  5p4e9  10074  5p5e10  10075  6p2e8  10076  6p3e9  10077  6p4e10  10078  7p2e9  10079  7p3e10  10080  8p2e10  10081  1mhlfehlf  10146  8th4div3  10147  halfpm6th  10148  nneo  10309  uzindOLD  10320  num0h  10348  numsuc  10350  dec10p  10367  numma  10369  nummac  10370  numma2c  10371  numadd  10372  numaddc  10373  nummul2c  10375  decaddci  10383  decbin0  10441  decbin2  10442  xmulm1  10816  xadddi2  10832  x2times  10834  elfzm1b  11080  quoremz  11191  quoremnn0ALT  11193  uzrdgxfr  11261  mulexpz  11375  expaddz  11379  sqrecii  11419  cu2  11434  i3  11437  iexpcyc  11440  binom2i  11445  binom2aiOLD  11446  binom3  11455  crreczi  11459  discr  11471  nn0opthlem1  11516  nn0opth2i  11519  faclbnd  11536  bcm1k  11561  bcp1nk  11563  bcpasc  11567  hashp1i  11627  hashxplem  11651  hashpw  11654  hashfun  11655  hashbc  11657  ccatlid  11703  revs1  11752  cats1cat  11780  imre  11868  crim  11875  remullem  11888  cnpart  12000  sqrneglem  12027  absexpz  12065  absimle  12069  sqreulem  12118  amgm2  12128  iseraltlem2  12431  iseraltlem3  12432  binomlem  12563  binom11  12566  arisum  12594  arisum2  12595  georeclim  12604  geo2sum  12605  mertenslem1  12616  mertens  12618  efzval  12658  resinval  12691  recosval  12692  efi4p  12693  tan0  12707  efival  12708  sinhval  12710  coshval  12711  cosadd  12721  cos2tsin  12735  ef01bndlem  12740  cos1bnd  12743  cos2bnd  12744  absefib  12754  efieq1re  12755  demoivreALT  12757  eirrlem  12758  rpnnen2lem3  12771  rpnnen2lem11  12779  ruclem7  12790  odd2np1  12863  3dvds  12867  divalglem2  12870  divalglem9  12876  m1bits  12907  sadcp1  12922  sadeq  12939  smupp1  12947  smumul  12960  gcdaddmlem  12983  nn0gcdsq  13099  phiprmpw  13120  prmdiv  13129  prmdiveq  13130  prmdivdiv  13131  pythagtriplem1  13145  pythagtriplem12  13155  pythagtriplem14  13157  pockthi  13230  infpnlem1  13233  prmreclem4  13242  4sqlem12  13279  4sqlem13  13280  4sqlem19  13286  vdwapun  13297  vdwlem6  13309  0hashbc  13330  dec5dvds  13355  dec5nprm  13357  dec2nprm  13358  modxai  13359  modxp1i  13361  mod2xnegi  13362  modsubi  13363  gcdmodi  13365  decexp2  13366  decsplit0b  13371  decsplit1  13373  decsplit  13374  karatsuba  13375  2exp6  13377  2exp8  13378  3exp3  13380  5prm  13386  7prm  13388  11prm  13392  prmlem2  13397  37prm  13398  43prm  13399  83prm  13400  139prm  13401  163prm  13402  317prm  13403  631prm  13404  1259lem1  13405  1259lem2  13406  1259lem3  13407  1259lem4  13408  1259lem5  13409  1259prm  13410  2503lem1  13411  2503lem2  13412  2503lem3  13413  2503prm  13414  4001lem1  13415  4001lem2  13416  4001lem3  13417  4001lem4  13418  4001prm  13419  pwsbas  13664  subsubc  14005  xpccatid  14240  subsubm  14712  mulg2  14854  subsubg  14918  oppgmnd  15105  gsumwrev  15117  sylow1lem1  15187  subgslw  15205  sylow3  15222  efginvrel2  15314  efgsfo  15326  frgpnabllem1  15439  ablfac1lem  15581  pgpfac1lem3  15590  pgpfaclem1  15594  mgpress  15614  opprrng  15691  unitsubm  15730  subsubrg  15849  lsslss  15992  gzrngunit  16719  expghm  16732  zrhval  16744  chrid  16763  resstopn  17204  cnmpt1res  17661  ressuss  18246  iscusp2  18285  ucnextcn  18287  txmetcnp  18530  rerest  18788  xrtgioo  18790  xrrest  18791  cnmpt2pc  18906  xrhmeo  18924  minveclem2  19280  ovolunlem1a  19345  ovolicc2lem4  19369  uniioombllem5  19432  iblabs  19673  iblabsr  19674  iblmulc2  19675  itgmulc2  19678  limcres  19726  dvfval  19737  dvreslem  19749  dvres2lem  19750  dvcnp2  19759  cpnres  19776  dvcobr  19785  dveflem  19816  lhop1lem  19850  lhop2  19852  dvcnvrelem2  19855  evlsval  19893  mpff  19915  plyun0  20069  coeeulem  20096  coeeu  20097  dvply1  20154  dvtaylp  20239  taylthlem2  20243  taylth  20244  dvradcnv  20290  pserdvlem2  20297  abelthlem8  20308  abelth  20310  sinhalfpilem  20327  cospi  20333  eulerid  20335  cos2pi  20337  ef2kpi  20339  sinhalfpip  20353  sinhalfpim  20354  coshalfpip  20355  coshalfpim  20356  sincosq3sgn  20361  sincosq4sgn  20362  tangtx  20366  sincos4thpi  20374  sincos6thpi  20376  sineq0  20382  tanregt0  20394  logm1  20436  abslogle  20466  tanarg  20467  logcnlem4  20489  advlogexp  20499  cxpsqr  20547  dvsqr  20581  cxpcn3  20585  root1cj  20593  cxpeq  20594  ang180lem1  20604  ang180lem2  20605  ang180lem3  20606  lawcos  20611  isosctrlem1  20615  isosctrlem2  20616  quad2  20632  1cubrlem  20634  1cubr  20635  dcubic1lem  20636  dcubic2  20637  mcubic  20640  binom4  20643  dquartlem1  20644  quart1lem  20648  quart1  20649  quartlem1  20650  asinlem  20661  asinlem2  20662  asinlem3a  20663  acosneg  20680  efiasin  20681  asinsinlem  20684  asinsin  20685  acoscos  20686  asin1  20687  acosbnd  20693  atancj  20703  efiatan  20705  atanlogaddlem  20706  efiatan2  20710  2efiatan  20711  tanatan  20712  cosatan  20714  atantan  20716  atanbndlem  20718  atans2  20724  dvatan  20728  atantayl  20730  atantayl2  20731  log2cnv  20737  log2tlbnd  20738  log2ublem2  20740  log2ublem3  20741  log2ub  20742  birthday  20746  jensenlem1  20778  amgmlem  20781  wilthlem1  20804  ftalem2  20809  ftalem5  20812  ftalem6  20813  basellem2  20817  basellem3  20818  basellem5  20820  basellem8  20823  basellem9  20824  mule1  20884  ppi1i  20904  musum  20929  ppiublem1  20939  ppiublem2  20940  ppiub  20941  chtublem  20948  chtub  20949  dchrptlem1  21001  dchrptlem2  21002  bclbnd  21017  bpos1  21020  bposlem6  21026  bposlem8  21028  bposlem9  21029  lgslem4  21036  lgsdir2lem1  21060  lgsdir2lem2  21061  lgsdir2lem4  21063  lgsdir2lem5  21064  lgsne0  21070  1lgs  21074  lgseisenlem1  21086  lgseisenlem2  21087  lgseisenlem3  21088  lgseisenlem4  21089  lgseisen  21090  lgsquadlem1  21091  lgsquadlem2  21092  lgsquad2lem1  21095  lgsquad2lem2  21096  m1lgs  21099  chebbnd1lem2  21117  chebbnd1lem3  21118  rplogsumlem2  21132  dchrisum0flblem1  21155  dchrisum0re  21160  mulog2sumlem2  21182  chpdifbndlem1  21200  pntpbnd1a  21232  pntpbnd2  21234  pntibndlem2  21238  pntibndlem3  21239  pntlemg  21245  pntlemk  21253  pntlemo  21254  usgraexvlem  21367  fargshiftlem  21574  constr3trllem3  21592  eupares  21650  konigsberg  21662  ex-fl  21708  addinv  21893  vc2  21987  vc0  22001  vcm  22003  vcnegneg  22006  nvnncan  22097  nvm1  22106  nvpi  22108  nvmtri  22113  nvge0  22116  ipval3  22158  ipidsq  22162  ip0i  22279  ip1ilem  22280  ip2i  22282  ipdirilem  22283  ipasslem10  22293  siilem1  22305  siii  22307  minvecolem2  22330  hvsubid  22481  hvaddsubval  22488  hvmul2negi  22503  hvadd12i  22512  hv2times  22516  hvnegdii  22517  hvaddcani  22520  hi01  22551  hisubcomi  22559  normlem0  22564  normlem1  22565  normlem3  22567  normlem9  22573  bcseqi  22575  normsqi  22587  norm-ii-i  22592  normsubi  22596  norm3difi  22602  norm3adifii  22603  normpar2i  22611  polid2i  22612  polidi  22613  chdmm2i  22933  chj12i  22977  spanunsni  23034  qlaxr5i  23090  osumcor2i  23099  spansnji  23101  pjadjii  23129  pjinormii  23131  pjsslem  23134  pjpythi  23177  mayete3i  23183  mayete3iOLD  23184  mayetes3i  23185  hoadd12i  23233  honegneg  23262  ho2times  23275  hoaddsubi  23277  hosd1i  23278  hosd2i  23279  honpncani  23283  lnopeq0lem1  23461  lnopunilem1  23466  lnophmlem2  23473  lnfn0i  23498  nmopcoadji  23557  nmopcoadj2i  23558  opsqrlem1  23596  opsqrlem5  23600  opsqrlem6  23601  pjclem3  23653  stadd3i  23704  mddmd2  23765  mdexchi  23791  cvexchlem  23824  atomli  23838  atordi  23840  atabs2i  23858  mdsymlem1  23859  iuninc  23964  sqsscirc1  24259  cnvordtrestixx  24264  raddcn  24268  xrge0iifhom  24276  xrge0mulc1cn  24280  xrge0tmd  24285  lmlimxrge0  24287  reust  24297  qqhucn  24329  rrhre  24340  logb1  24356  brfae  24552  cndprobnul  24648  isrrvv  24654  ballotlem1  24697  ballotlem2  24699  ballotlemodife  24708  ballotlemi1  24713  ballotlemii  24714  ballotlemic  24717  ballotlem1c  24718  ballotlemfrceq  24739  ballotth  24748  lgamgulmlem2  24767  lgamgulmlem5  24770  lgambdd  24774  subfacp1lem1  24818  subfacp1lem5  24823  subfacp1lem6  24824  subfaclim  24827  cvmliftlem5  24929  cvmliftlem8  24932  cvmliftlem10  24934  cvmliftlem13  24936  cvmlift2lem6  24948  cvmlift2lem12  24954  elfzp1b  25069  prodfrec  25176  fprodm1s  25246  fprodp1s  25247  fallfacfwd  25303  0risefac  25305  axsegconlem1  25760  ax5seglem7  25778  axlowdimlem3  25787  axlowdimlem16  25800  axlowdimlem17  25801  bpolydiflem  26004  bpoly2  26007  bpoly3  26008  bpoly4  26009  fsumcube  26010  mblfinlem2  26144  ismblfin  26146  itg2addnclem3  26157  iblabsnc  26168  iblmulc2nc  26169  itgmulc2nc  26172  ftc1cnnc  26178  fdc  26339  csbrn  26346  heiborlem4  26413  heiborlem6  26415  pellexlem5  26786  reglog1  26849  jm2.23  26957  jm2.27c  26968  lnmlsslnm  27047  lmhmlnmsplit  27053  psgnunilem2  27286  matvsca2  27346  cntzsdrg  27378  lhe4.4ex1a  27414  itgsinexplem1  27615  stoweidlem11  27627  stoweidlem13  27629  stoweidlem26  27642  stoweidlem34  27650  wallispilem4  27684  wallispi2lem1  27687  wallispi2lem2  27688  stirlinglem11  27700  swrdccatin2  28018  sinh-conventional  28196  onetansqsecsq  28218  cotsqcscsq  28219  dpfrac1  28229  dalem24  30179  pmod2iN  30331  cdleme9  30735  cdleme20aN  30791  cdleme22e  30826  cdleme22eALTN  30827  cdleme25cv  30840  cdleme29b  30857  cdlemh1  31297  cdlemh2  31298  cdlemk35  31394  cdlemkid1  31404
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043
  Copyright terms: Public domain W3C validator