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

Theorem oveq1i 6058
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 6055 . 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 6048
This theorem is referenced by:  caov12  6242  caov411  6246  omopthlem1  6865  map1  7152  pw2eng  7181  cnfcomlem  7620  cnfcom2  7623  infxpenc2  7867  adderpqlem  8795  addassnq  8799  distrnq  8802  halfnq  8817  archnq  8821  addclprlem2  8858  addcmpblnr  8911  ltsrpr  8916  m1m1sr  8932  recexsrlem  8942  sqgt0sr  8945  map2psrpr  8949  axi2m1  8998  axcnre  9003  mul02lem2  9207  addid1  9210  cnegex2  9212  addid2  9213  negsubdi  9321  mulneg1  9434  recextlem1  9616  recdiv  9684  divmul13i  9739  2p2e4  10062  2times  10063  3p2e5  10075  3p3e6  10076  4p2e6  10077  4p3e7  10078  4p4e8  10079  5p2e7  10080  5p3e8  10081  5p4e9  10082  5p5e10  10083  6p2e8  10084  6p3e9  10085  6p4e10  10086  7p2e9  10087  7p3e10  10088  8p2e10  10089  1mhlfehlf  10154  8th4div3  10155  halfpm6th  10156  nneo  10317  uzindOLD  10328  num0h  10356  numsuc  10358  dec10p  10375  numma  10377  nummac  10378  numma2c  10379  numadd  10380  numaddc  10381  nummul2c  10383  decaddci  10391  decbin0  10449  decbin2  10450  xmulm1  10824  xadddi2  10840  x2times  10842  elfzm1b  11088  quoremz  11199  quoremnn0ALT  11201  uzrdgxfr  11269  mulexpz  11383  expaddz  11387  sqrecii  11427  cu2  11442  i3  11445  iexpcyc  11448  binom2i  11453  binom2aiOLD  11454  binom3  11463  crreczi  11467  discr  11479  nn0opthlem1  11524  nn0opth2i  11527  faclbnd  11544  bcm1k  11569  bcp1nk  11571  bcpasc  11575  hashp1i  11635  hashxplem  11659  hashpw  11662  hashfun  11663  hashbc  11665  ccatlid  11711  revs1  11760  cats1cat  11788  imre  11876  crim  11883  remullem  11896  cnpart  12008  sqrneglem  12035  absexpz  12073  absimle  12077  sqreulem  12126  amgm2  12136  iseraltlem2  12439  iseraltlem3  12440  binomlem  12571  binom11  12574  arisum  12602  arisum2  12603  georeclim  12612  geo2sum  12613  mertenslem1  12624  mertens  12626  efzval  12666  resinval  12699  recosval  12700  efi4p  12701  tan0  12715  efival  12716  sinhval  12718  coshval  12719  cosadd  12729  cos2tsin  12743  ef01bndlem  12748  cos1bnd  12751  cos2bnd  12752  absefib  12762  efieq1re  12763  demoivreALT  12765  eirrlem  12766  rpnnen2lem3  12779  rpnnen2lem11  12787  ruclem7  12798  odd2np1  12871  3dvds  12875  divalglem2  12878  divalglem9  12884  m1bits  12915  sadcp1  12930  sadeq  12947  smupp1  12955  smumul  12968  gcdaddmlem  12991  nn0gcdsq  13107  phiprmpw  13128  prmdiv  13137  prmdiveq  13138  prmdivdiv  13139  pythagtriplem1  13153  pythagtriplem12  13163  pythagtriplem14  13165  pockthi  13238  infpnlem1  13241  prmreclem4  13250  4sqlem12  13287  4sqlem13  13288  4sqlem19  13294  vdwapun  13305  vdwlem6  13317  0hashbc  13338  dec5dvds  13363  dec5nprm  13365  dec2nprm  13366  modxai  13367  modxp1i  13369  mod2xnegi  13370  modsubi  13371  gcdmodi  13373  decexp2  13374  decsplit0b  13379  decsplit1  13381  decsplit  13382  karatsuba  13383  2exp6  13385  2exp8  13386  3exp3  13388  5prm  13394  7prm  13396  11prm  13400  prmlem2  13405  37prm  13406  43prm  13407  83prm  13408  139prm  13409  163prm  13410  317prm  13411  631prm  13412  1259lem1  13413  1259lem2  13414  1259lem3  13415  1259lem4  13416  1259lem5  13417  1259prm  13418  2503lem1  13419  2503lem2  13420  2503lem3  13421  2503prm  13422  4001lem1  13423  4001lem2  13424  4001lem3  13425  4001lem4  13426  4001prm  13427  pwsbas  13672  subsubc  14013  xpccatid  14248  subsubm  14720  mulg2  14862  subsubg  14926  oppgmnd  15113  gsumwrev  15125  sylow1lem1  15195  subgslw  15213  sylow3  15230  efginvrel2  15322  efgsfo  15334  frgpnabllem1  15447  ablfac1lem  15589  pgpfac1lem3  15598  pgpfaclem1  15602  mgpress  15622  opprrng  15699  unitsubm  15738  subsubrg  15857  lsslss  16000  gzrngunit  16727  expghm  16740  zrhval  16752  chrid  16771  resstopn  17212  cnmpt1res  17669  ressuss  18254  iscusp2  18293  ucnextcn  18295  txmetcnp  18538  rerest  18796  xrtgioo  18798  xrrest  18799  cnmpt2pc  18914  xrhmeo  18932  minveclem2  19288  ovolunlem1a  19353  ovolicc2lem4  19377  uniioombllem5  19440  iblabs  19681  iblabsr  19682  iblmulc2  19683  itgmulc2  19686  limcres  19734  dvfval  19745  dvreslem  19757  dvres2lem  19758  dvcnp2  19767  cpnres  19784  dvcobr  19793  dveflem  19824  lhop1lem  19858  lhop2  19860  dvcnvrelem2  19863  evlsval  19901  mpff  19923  plyun0  20077  coeeulem  20104  coeeu  20105  dvply1  20162  dvtaylp  20247  taylthlem2  20251  taylth  20252  dvradcnv  20298  pserdvlem2  20305  abelthlem8  20316  abelth  20318  sinhalfpilem  20335  cospi  20341  eulerid  20343  cos2pi  20345  ef2kpi  20347  sinhalfpip  20361  sinhalfpim  20362  coshalfpip  20363  coshalfpim  20364  sincosq3sgn  20369  sincosq4sgn  20370  tangtx  20374  sincos4thpi  20382  sincos6thpi  20384  sineq0  20390  tanregt0  20402  logm1  20444  abslogle  20474  tanarg  20475  logcnlem4  20497  advlogexp  20507  cxpsqr  20555  dvsqr  20589  cxpcn3  20593  root1cj  20601  cxpeq  20602  ang180lem1  20612  ang180lem2  20613  ang180lem3  20614  lawcos  20619  isosctrlem1  20623  isosctrlem2  20624  quad2  20640  1cubrlem  20642  1cubr  20643  dcubic1lem  20644  dcubic2  20645  mcubic  20648  binom4  20651  dquartlem1  20652  quart1lem  20656  quart1  20657  quartlem1  20658  asinlem  20669  asinlem2  20670  asinlem3a  20671  acosneg  20688  efiasin  20689  asinsinlem  20692  asinsin  20693  acoscos  20694  asin1  20695  acosbnd  20701  atancj  20711  efiatan  20713  atanlogaddlem  20714  efiatan2  20718  2efiatan  20719  tanatan  20720  cosatan  20722  atantan  20724  atanbndlem  20726  atans2  20732  dvatan  20736  atantayl  20738  atantayl2  20739  log2cnv  20745  log2tlbnd  20746  log2ublem2  20748  log2ublem3  20749  log2ub  20750  birthday  20754  jensenlem1  20786  amgmlem  20789  wilthlem1  20812  ftalem2  20817  ftalem5  20820  ftalem6  20821  basellem2  20825  basellem3  20826  basellem5  20828  basellem8  20831  basellem9  20832  mule1  20892  ppi1i  20912  musum  20937  ppiublem1  20947  ppiublem2  20948  ppiub  20949  chtublem  20956  chtub  20957  dchrptlem1  21009  dchrptlem2  21010  bclbnd  21025  bpos1  21028  bposlem6  21034  bposlem8  21036  bposlem9  21037  lgslem4  21044  lgsdir2lem1  21068  lgsdir2lem2  21069  lgsdir2lem4  21071  lgsdir2lem5  21072  lgsne0  21078  1lgs  21082  lgseisenlem1  21094  lgseisenlem2  21095  lgseisenlem3  21096  lgseisenlem4  21097  lgseisen  21098  lgsquadlem1  21099  lgsquadlem2  21100  lgsquad2lem1  21103  lgsquad2lem2  21104  m1lgs  21107  chebbnd1lem2  21125  chebbnd1lem3  21126  rplogsumlem2  21140  dchrisum0flblem1  21163  dchrisum0re  21168  mulog2sumlem2  21190  chpdifbndlem1  21208  pntpbnd1a  21240  pntpbnd2  21242  pntibndlem2  21246  pntibndlem3  21247  pntlemg  21253  pntlemk  21261  pntlemo  21262  usgraexvlem  21375  fargshiftlem  21582  constr3trllem3  21600  eupares  21658  konigsberg  21670  ex-fl  21716  addinv  21901  vc2  21995  vc0  22009  vcm  22011  vcnegneg  22014  nvnncan  22105  nvm1  22114  nvpi  22116  nvmtri  22121  nvge0  22124  ipval3  22166  ipidsq  22170  ip0i  22287  ip1ilem  22288  ip2i  22290  ipdirilem  22291  ipasslem10  22301  siilem1  22313  siii  22315  minvecolem2  22338  hvsubid  22489  hvaddsubval  22496  hvmul2negi  22511  hvadd12i  22520  hv2times  22524  hvnegdii  22525  hvaddcani  22528  hi01  22559  hisubcomi  22567  normlem0  22572  normlem1  22573  normlem3  22575  normlem9  22581  bcseqi  22583  normsqi  22595  norm-ii-i  22600  normsubi  22604  norm3difi  22610  norm3adifii  22611  normpar2i  22619  polid2i  22620  polidi  22621  chdmm2i  22941  chj12i  22985  spanunsni  23042  qlaxr5i  23098  osumcor2i  23107  spansnji  23109  pjadjii  23137  pjinormii  23139  pjsslem  23142  pjpythi  23185  mayete3i  23191  mayete3iOLD  23192  mayetes3i  23193  hoadd12i  23241  honegneg  23270  ho2times  23283  hoaddsubi  23285  hosd1i  23286  hosd2i  23287  honpncani  23291  lnopeq0lem1  23469  lnopunilem1  23474  lnophmlem2  23481  lnfn0i  23506  nmopcoadji  23565  nmopcoadj2i  23566  opsqrlem1  23604  opsqrlem5  23608  opsqrlem6  23609  pjclem3  23661  stadd3i  23712  mddmd2  23773  mdexchi  23799  cvexchlem  23832  atomli  23846  atordi  23848  atabs2i  23866  mdsymlem1  23867  iuninc  23972  sqsscirc1  24267  cnvordtrestixx  24272  raddcn  24276  xrge0iifhom  24284  xrge0mulc1cn  24288  xrge0tmd  24293  lmlimxrge0  24295  reust  24305  qqhucn  24337  rrhre  24348  logb1  24364  brfae  24560  cndprobnul  24656  isrrvv  24662  ballotlem1  24705  ballotlem2  24707  ballotlemodife  24716  ballotlemi1  24721  ballotlemii  24722  ballotlemic  24725  ballotlem1c  24726  ballotlemfrceq  24747  ballotth  24756  lgamgulmlem2  24775  lgamgulmlem5  24778  lgambdd  24782  subfacp1lem1  24826  subfacp1lem5  24831  subfacp1lem6  24832  subfaclim  24835  cvmliftlem5  24937  cvmliftlem8  24940  cvmliftlem10  24942  cvmliftlem13  24944  cvmlift2lem6  24956  cvmlift2lem12  24962  elfzp1b  25077  prodfrec  25184  fprodm1s  25254  fprodp1s  25255  fallfacfwd  25311  0risefac  25313  axsegconlem1  25768  ax5seglem7  25786  axlowdimlem3  25795  axlowdimlem16  25808  axlowdimlem17  25809  bpolydiflem  26012  bpoly2  26015  bpoly3  26016  bpoly4  26017  fsumcube  26018  mblfinlem2  26152  ismblfin  26154  itg2addnclem3  26165  iblabsnc  26176  iblmulc2nc  26177  itgmulc2nc  26180  ftc1cnnc  26186  fdc  26347  csbrn  26354  heiborlem4  26421  heiborlem6  26423  pellexlem5  26794  reglog1  26857  jm2.23  26965  jm2.27c  26976  lnmlsslnm  27055  lmhmlnmsplit  27061  psgnunilem2  27294  matvsca2  27354  cntzsdrg  27386  lhe4.4ex1a  27422  itgsinexplem1  27623  stoweidlem11  27635  stoweidlem13  27637  stoweidlem26  27650  stoweidlem34  27658  wallispilem4  27692  wallispi2lem1  27695  wallispi2lem2  27696  stirlinglem11  27708  swrdccatin2  28026  sinh-conventional  28204  onetansqsecsq  28226  cotsqcscsq  28227  dpfrac1  28237  dalem24  30191  pmod2iN  30343  cdleme9  30747  cdleme20aN  30803  cdleme22e  30838  cdleme22eALTN  30839  cdleme25cv  30852  cdleme29b  30869  cdlemh1  31309  cdlemh2  31310  cdlemk35  31406  cdlemkid1  31416
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 2393
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 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-rex 2680  df-rab 2683  df-v 2926  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-sn 3788  df-pr 3789  df-op 3791  df-uni 3984  df-br 4181  df-iota 5385  df-fv 5429  df-ov 6051
  Copyright terms: Public domain W3C validator