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

Theorem oveq1i 7228
Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
Hypothesis
Ref Expression
oveq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
oveq1i (𝐴𝐹𝐶) = (𝐵𝐹𝐶)

Proof of Theorem oveq1i
StepHypRef Expression
1 oveq1i.1 . 2 𝐴 = 𝐵
2 oveq1 7225 . 2 (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
31, 2ax-mp 5 1 (𝐴𝐹𝐶) = (𝐵𝐹𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1543  (class class class)co 7218
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070  df-v 3415  df-dif 3874  df-un 3876  df-in 3878  df-ss 3888  df-nul 4243  df-if 4445  df-sn 4547  df-pr 4549  df-op 4553  df-uni 4825  df-br 5059  df-iota 6343  df-fv 6393  df-ov 7221
This theorem is referenced by:  caov12  7441  caov411  7445  omopthlem1  8389  map1  8722  pw2eng  8756  fsuppunbi  9011  cnfcomlem  9319  cnfcom2  9322  infxpenc2  9641  adderpqlem  10573  addassnq  10577  distrnq  10580  halfnq  10595  archnq  10599  addclprlem2  10636  addcmpblnr  10688  ltsrpr  10696  m1m1sr  10712  recexsrlem  10722  sqgt0sr  10725  map2psrpr  10729  axi2m1  10778  axcnre  10783  mul02lem2  11014  addid1  11017  cnegex2  11019  addid2  11020  mvrraddi  11100  mvlladdi  11101  negsubdi  11139  mulneg1  11273  recextlem1  11467  recdiv  11543  divmul13i  11598  mvllmuli  11670  2p2e4  11970  2times  11971  1p2e3  11978  3p2e5  11986  3p3e6  11987  4p2e6  11988  4p3e7  11989  4p4e8  11990  5p2e7  11991  5p3e8  11992  5p4e9  11993  6p2e8  11994  6p3e9  11995  7p2e9  11996  1mhlfehlf  12054  8th4div3  12055  halfpm6th  12056  nneo  12266  9p1e10  12300  dfdec10  12301  num0h  12310  numsuc  12312  dec10p  12341  numma  12342  nummac  12343  numma2c  12344  numadd  12345  numaddc  12346  nummul2c  12348  decaddci  12359  decsubi  12361  5p5e10  12369  6p4e10  12370  7p3e10  12373  8p2e10  12378  decbin0  12438  decbin2  12439  xmulm1  12876  xadddi2  12892  x2times  12894  elfzp1b  13194  elfzm1b  13195  fz1ssfz0  13213  fz0to4untppr  13220  fz0sn0fz1  13234  fz0add1fz1  13317  elfz0lmr  13362  fldiv4p1lem1div2  13415  quoremz  13433  quoremnn0ALT  13435  uzrdgxfr  13545  mulexpz  13680  expaddz  13684  sqrecii  13757  sq4e2t8  13773  cu2  13774  i3  13777  iexpcyc  13780  binom2i  13785  binom3  13796  crreczi  13800  discr  13812  3dec  13837  nn0opthlem1  13839  nn0opth2i  13842  faclbnd  13861  bcp1nk  13888  bcpasc  13892  hashp1i  13975  hashxplem  14005  hashpw  14008  hashfun  14009  hashbc  14022  ccatlid  14148  pfxccatin12lem2c  14300  revs1  14335  cats1cat  14431  cats2cat  14432  lsws2  14474  lsws3  14475  lsws4  14476  s3s4  14503  s2s5  14504  s5s2  14505  imre  14676  crim  14683  remullem  14696  cnpart  14808  sqrtneglem  14835  absexpz  14874  absimle  14878  sqreulem  14928  amgm2  14938  iseraltlem2  15251  iseraltlem3  15252  modfsummod  15363  binomlem  15398  binom11  15401  arisum  15429  arisum2  15430  pwdif  15437  georeclim  15441  geo2sum  15442  mertenslem1  15453  mertens  15455  prodfrec  15464  fprodm1s  15537  fprodp1s  15538  fprodmodd  15564  fallfacfwd  15603  0risefac  15605  bpolydiflem  15621  bpoly2  15624  bpoly3  15625  bpoly4  15626  fsumcube  15627  efzval  15668  resinval  15701  recosval  15702  efi4p  15703  tan0  15717  efival  15718  sinhval  15720  coshval  15721  cosadd  15731  cos2tsin  15745  ef01bndlem  15750  cos1bnd  15753  cos2bnd  15754  absefib  15764  efieq1re  15765  demoivreALT  15767  eirrlem  15770  rpnnen2lem3  15782  rpnnen2lem11  15790  ruclem7  15802  3dvds  15897  3dvdsdec  15898  3dvds2dec  15899  odd2np1  15907  nn0o1gt2  15947  nn0o  15949  pwp1fsum  15957  divalglem2  15961  divalglem9  15967  flodddiv4  15979  m1bits  16004  sadcp1  16019  sadeq  16036  smupp1  16044  smumul  16057  gcdaddmlem  16088  3lcm2e6woprm  16177  nn0gcdsq  16313  phiprmpw  16334  prmdiv  16343  prmdiveq  16344  pythagtriplem1  16374  pythagtriplem12  16384  pythagtriplem14  16386  pockthi  16465  infpnlem1  16468  prmreclem4  16477  4sqlem12  16514  4sqlem13  16515  4sqlem19  16521  vdwapun  16532  vdwlem6  16544  0hashbc  16565  prmo2  16598  prmo3  16599  dec5dvds  16622  dec5nprm  16624  dec2nprm  16625  modxai  16626  modxp1i  16628  mod2xnegi  16629  modsubi  16630  gcdmodi  16632  decexp2  16633  decsplit0b  16638  decsplit1  16640  decsplit  16641  karatsuba  16642  2exp7  16646  2exp8  16647  3exp3  16650  5prm  16667  7prm  16669  11prm  16673  prmlem2  16678  37prm  16679  43prm  16680  83prm  16681  139prm  16682  163prm  16683  317prm  16684  631prm  16685  prmo5  16687  1259lem1  16689  1259lem2  16690  1259lem3  16691  1259lem4  16692  1259lem5  16693  2503lem1  16695  2503lem2  16696  2503lem3  16697  2503prm  16698  4001lem1  16699  4001lem2  16700  4001lem3  16701  4001lem4  16702  4001prm  16703  pwsbas  16997  rcaninv  17304  subsubc  17364  xpccatid  17700  subsubm  18248  smndex2dnrinv  18347  mulg2  18506  subsubg  18571  oppgmnd  18751  gsumwrev  18763  psgnunilem2  18892  sylow1lem1  18992  subgslw  19010  sylow3  19027  efginvrel2  19122  efgsfo  19134  frgpnabllem1  19263  gsumzaddlem  19311  gsummptfzsplitl  19323  gsummpt1n0  19355  dprdfid  19409  ablfac1lem  19460  pgpfac1lem3  19469  pgpfaclem1  19473  ablsimpgfindlem1  19499  mgpress  19520  srgbinomlem4  19563  opprring  19654  unitsubm  19693  subsubrg  19831  cntzsdrg  19851  subdrgint  19852  lsslss  20003  xrsnsgrp  20404  gzrngunit  20434  expghm  20467  chrid  20497  zrhpsgnmhm  20551  psgndiflemA  20568  frlmip  20745  frlmphl  20748  evlsval  21051  mpff  21069  coe1fzgsumdlem  21227  evl1gsumdlem  21277  matvsca2  21330  mattposvs  21357  m2detleiblem3  21531  m2detleiblem4  21532  cpmidpmat  21775  resstopn  22088  cnmpt1res  22578  ressuss  23165  iscusp2  23204  ucnextcn  23206  txmetcnp  23450  rerest  23706  xrtgioo  23708  xrrest  23709  cnmpopc  23830  xrhmeo  23848  clmvs2  23996  clmnegneg  24006  ncvsm1  24056  ncvspi  24058  cphassir  24117  cphipval2  24143  reust  24283  rrxprds  24291  csbren  24301  rrxdsfi  24313  minveclem2  24328  ovolunlem1a  24398  ovolicc2lem4  24422  uniioombllem5  24489  iblabs  24731  iblabsr  24732  iblmulc2  24733  itgmulc2  24736  limcres  24788  dvfval  24799  dvreslem  24811  dvres2lem  24812  dvcnp2  24822  cpnres  24839  dvcobr  24848  dveflem  24881  lhop1lem  24915  lhop2  24917  dvcnvrelem2  24920  plyun0  25096  coeeulem  25123  coeeu  25124  dvply1  25182  dvtaylp  25267  taylthlem2  25271  taylth  25272  dvradcnv  25318  pserdvlem2  25325  abelthlem8  25336  abelth  25338  sinhalfpilem  25358  cospi  25367  eulerid  25369  cos2pi  25371  ef2kpi  25373  sinhalfpip  25387  sinhalfpim  25388  coshalfpip  25389  coshalfpim  25390  sincosq3sgn  25395  sincosq4sgn  25396  tangtx  25400  sincos4thpi  25408  sincos6thpi  25410  sineq0  25418  tanregt0  25433  logm1  25482  abslogle  25511  tanarg  25512  logcnlem4  25538  advlogexp  25548  cxpsqrt  25596  dvsqrt  25633  dvcnsqrt  25635  cxpcn3  25639  root1cj  25647  cxpeq  25648  logb1  25657  2logb9irr  25683  sqrt2cxp2logb9e3  25687  ang180lem1  25697  ang180lem2  25698  ang180lem3  25699  lawcos  25704  isosctrlem1  25706  isosctrlem2  25707  quad2  25727  1cubrlem  25729  1cubr  25730  dcubic2  25732  mcubic  25735  binom4  25738  dquartlem1  25739  quart1lem  25743  quart1  25744  quartlem1  25745  asinlem  25756  asinlem2  25757  asinlem3a  25758  acosneg  25775  efiasin  25776  asinsinlem  25779  asinsin  25780  acoscos  25781  asin1  25782  acosbnd  25788  atancj  25798  efiatan  25800  atanlogaddlem  25801  efiatan2  25805  2efiatan  25806  tanatan  25807  cosatan  25809  atantan  25811  atanbndlem  25813  atans2  25819  dvatan  25823  atantayl  25825  atantayl2  25826  log2cnv  25832  log2tlbnd  25833  log2ublem2  25835  log2ublem3  25836  log2ub  25837  birthday  25842  jensenlem1  25874  amgmlem  25877  lgamgulmlem2  25917  lgamgulmlem5  25920  lgambdd  25924  ftalem2  25961  ftalem5  25964  ftalem6  25965  basellem2  25969  basellem3  25970  basellem5  25972  basellem8  25975  basellem9  25976  mule1  26035  ppi1i  26055  musum  26078  ppiublem1  26088  ppiub  26090  chtublem  26097  chtub  26098  dchrptlem1  26150  dchrptlem2  26151  bclbnd  26166  bposlem6  26175  bposlem8  26177  bposlem9  26178  lgsdir2lem1  26211  lgsdir2lem2  26212  lgsdir2lem4  26214  lgsdir2lem5  26215  lgsne0  26221  1lgs  26226  gausslemma2dlem0e  26246  gausslemma2dlem0f  26247  gausslemma2dlem3  26254  gausslemma2d  26260  lgseisenlem1  26261  lgseisenlem2  26262  lgseisenlem3  26263  lgseisenlem4  26264  lgseisen  26265  lgsquadlem1  26266  lgsquadlem2  26267  lgsquad2lem1  26270  lgsquad2lem2  26271  m1lgs  26274  2lgslem3a  26282  2lgslem3b  26283  2lgslem3c  26284  2lgslem3d  26285  2lgsoddprmlem3a  26296  2lgsoddprmlem3b  26297  2lgsoddprmlem3c  26298  2lgsoddprmlem3d  26299  addsqnreup  26329  chebbnd1lem2  26356  chebbnd1lem3  26357  rplogsumlem2  26371  dchrisum0flblem1  26394  dchrisum0re  26399  mulog2sumlem2  26421  chpdifbndlem1  26439  pntpbnd1a  26471  pntpbnd2  26473  pntibndlem2  26477  pntibndlem3  26478  pntlemg  26484  pntlemk  26492  pntlemo  26493  axsegconlem1  27013  ax5seglem7  27031  axlowdimlem3  27040  axlowdimlem16  27053  axlowdimlem17  27054  elntg2  27081  vdegp1bi  27630  vtxdginducedm1  27636  wlkp1lem1  27766  spthispth  27818  2wlkdlem1  28014  2pthd  28029  clwlkclwwlkfo  28097  3wlkdlem1  28247  3pthd  28262  eucrct2eupth  28333  numclwwlk5  28476  numclwwlk7  28479  frgrregord013  28483  ex-fl  28535  ex-mod  28537  ex-exp  28538  ex-bc  28540  ex-lcm  28546  ex-ind-dvds  28549  vc2OLD  28654  vc0  28660  vcm  28662  nvm1  28751  nvpi  28753  nvmtri  28757  nvge0  28759  ipval3  28795  ipidsq  28796  ip0i  28911  ip1ilem  28912  ip2i  28914  ipdirilem  28915  ipasslem10  28925  siilem1  28937  siii  28939  minvecolem2  28961  hvsubid  29112  hvaddsubval  29119  hvmul2negi  29134  hvadd12i  29143  hv2times  29147  hvnegdii  29148  hvaddcani  29151  hi01  29182  hisubcomi  29190  normlem0  29195  normlem1  29196  normlem3  29198  normlem9  29204  bcseqi  29206  normsqi  29218  norm-ii-i  29223  normsubi  29227  norm3difi  29233  norm3adifii  29234  normpar2i  29242  polid2i  29243  polidi  29244  chdmm2i  29564  chj12i  29608  spanunsni  29665  qlaxr5i  29721  osumcor2i  29730  spansnji  29732  pjadjii  29760  pjinormii  29762  pjsslem  29765  pjpythi  29808  mayete3i  29814  mayetes3i  29815  hoadd12i  29863  honegneg  29892  ho2times  29905  hoaddsubi  29907  hosd1i  29908  hosd2i  29909  honpncani  29913  lnopeq0lem1  30091  lnopunilem1  30096  lnophmlem2  30103  lnfn0i  30128  nmopcoadji  30187  nmopcoadj2i  30188  opsqrlem1  30226  opsqrlem5  30230  opsqrlem6  30231  pjclem3  30283  stadd3i  30334  mddmd2  30395  mdexchi  30421  cvexchlem  30454  atomli  30468  atordi  30470  atabs2i  30488  mdsymlem1  30489  iuninc  30624  suppss2f  30698  suppss3  30784  dfdec100  30869  dpfrac1  30891  decdiv10  30895  dpmul100  30896  dp3mul10  30897  dpmul1000  30898  dpexpp1  30907  dpadd2  30909  dpadd  30910  dpmul  30912  dpmul4  30913  threehalves  30914  1mhdrd  30915  pfxlsw2ccat  30949  cyc2fv1  31112  cyc2fv2  31113  cycpmco2lem4  31120  cycpmco2lem5  31121  cyc3fv1  31128  cyc3fv2  31129  cyc3fv3  31130  archirngz  31167  gsumvsca2  31204  nn0omnd  31264  nn0archi  31266  xrge0slmod  31267  fedgmullem1  31429  fedgmullem2  31430  fedgmul  31431  lmatfvlem  31484  sqsscirc1  31577  cnvordtrestixx  31582  raddcn  31598  xrge0iifhom  31606  xrge0mulc1cn  31610  xrge0tmd  31614  lmlimxrge0  31617  qqhucn  31659  rrhcn  31664  qqtopn  31678  rrhqima  31681  brfae  31933  inelcarsg  31995  cndprobnul  32121  isrrvv  32127  ballotlem1  32170  ballotlem2  32172  ballotlemi1  32186  ballotlemii  32187  ballotlemic  32190  ballotlem1c  32191  ballotlemfrceq  32212  ballotth  32221  ofcs2  32241  signsvtn0  32266  signstfveq0  32273  signsvtp  32279  signsvtn  32280  signsvfpn  32281  signsvfnn  32282  signshf  32284  hashreprin  32317  reprfz1  32321  chtvalz  32326  breprexp  32330  breprexpnat  32331  hgt750lemd  32345  hgt750lem  32348  hgt750lem2  32349  subfacp1lem1  32859  subfacp1lem5  32864  subfacp1lem6  32865  subfaclim  32868  cvmliftlem5  32969  cvmliftlem8  32972  cvmliftlem10  32974  cvmliftlem13  32976  cvmlift2lem6  32988  cvmlift2lem12  32994  problem1  33341  problem2  33342  problem4  33344  quad3  33346  iexpire  33424  sin2h  35509  poimirlem16  35535  poimirlem17  35536  poimirlem18  35537  poimirlem19  35538  poimirlem20  35539  poimirlem21  35540  poimirlem22  35541  poimirlem26  35545  mblfinlem3  35558  ismblfin  35560  itg2addnclem3  35572  iblabsnc  35583  iblmulc2nc  35584  itgmulc2nc  35587  ftc1cnnc  35591  ftc1anclem6  35597  ftc1anclem7  35598  ftc1anclem8  35599  dvasin  35603  fdc  35645  heiborlem4  35714  heiborlem6  35716  dalem24  37453  pmod2iN  37605  cdleme9  38009  cdleme20aN  38065  cdleme22e  38100  cdleme22eALTN  38101  cdleme25cv  38114  cdleme29b  38131  cdlemh1  38571  cdlemh2  38572  cdlemk35  38668  cdlemkid1  38678  12gcd5e1  39750  60gcd7e1  39752  420gcd8e4  39753  12lcm5e60  39755  420lcm8e840  39758  lcm1un  39760  lcm2un  39761  lcm3un  39762  lcm4un  39763  lcm5un  39764  lcm6un  39765  lcm7un  39766  lcm8un  39767  3factsumint1  39768  3factsumint3  39770  lcmineqlem10  39785  3exp7  39800  3lexlogpow5ineq1  39801  3lexlogpow5ineq5  39807  aks4d1p1  39822  5bc2eq10  39828  2ap1caineq  39831  sqmid3api  40026  sqn5i  40028  sqdeccom12  40032  235t711  40034  nn0expgcd  40051  re1m1e0m0  40096  readdid2  40102  remul02  40104  sn-1ticom  40132  sn-mulid2  40133  sn-0tie0  40137  sn-mul02  40138  sn-inelr  40151  flt4lem5e  40204  pellexlem5  40366  reglog1  40429  jm2.23  40529  jm2.27c  40540  lnmlsslnm  40617  lmhmlnmsplit  40623  areaquad  40758  resqrtvalex  40937  imsqrtvalex  40938  cotrclrcl  41035  inductionexd  41450  hashnzfz2  41620  lhe4.4ex1a  41628  binomcxplemdvsum  41654  binomcxplemnotnn0  41655  binomcxp  41656  sineq0ALT  42238  unirnmapsn  42435  fzisoeu  42520  fsummulc1f  42795  fprodexp  42818  constlimc  42848  sumnnodd  42854  limcresiooub  42866  limcresioolb  42867  cncfshiftioo  43116  fperdvper  43143  dvnmul  43167  dvmptfprod  43169  itgsinexplem1  43178  stoweidlem11  43235  stoweidlem13  43237  stoweidlem26  43250  stoweidlem34  43258  wallispilem4  43292  wallispi2lem1  43295  wallispi2lem2  43296  stirlinglem11  43308  dirkerper  43320  dirkertrigeqlem1  43322  dirkertrigeqlem3  43324  dirkercncflem1  43327  dirkercncflem4  43330  fourierdlem30  43361  fourierdlem32  43363  fourierdlem33  43364  fourierdlem42  43373  fourierdlem46  43376  fourierdlem47  43377  fourierdlem57  43387  fourierdlem60  43390  fourierdlem61  43391  fourierdlem62  43392  fourierdlem68  43398  fourierdlem73  43403  fourierdlem79  43409  fourierdlem89  43419  fourierdlem90  43420  fourierdlem91  43421  fourierdlem96  43426  fourierdlem97  43427  fourierdlem98  43428  fourierdlem99  43429  fourierdlem100  43430  fourierdlem103  43433  fourierdlem104  43434  fourierdlem108  43438  fourierdlem110  43440  fourierdlem113  43443  sqwvfoura  43452  sqwvfourb  43453  fourierswlem  43454  fouriersw  43455  fouriercn  43456  etransclem4  43462  etransclem7  43465  etransclem23  43481  etransclem24  43482  etransclem25  43483  etransclem26  43484  etransclem31  43489  etransclem32  43490  etransclem35  43493  etransclem37  43495  etransclem46  43504  rrndistlt  43514  sge0tsms  43601  sge0xaddlem2  43655  vonioolem2  43902  1t10e1p1e11  44483  deccarry  44484  1fzopredsuc  44497  m1mod0mod1  44502  iccpartgt  44560  fmtno0  44673  fmtno1  44674  fmtnorec2  44676  fmtno2  44683  fmtno3  44684  fmtno4  44685  fmtno5  44690  257prm  44694  fmtnofac1  44703  fmtno4prmfac  44705  fmtno4prmfac193  44706  fmtno4nprmfac193  44707  m2prm  44724  m3prm  44725  flsqrt5  44727  3ndvds4  44728  139prmALT  44729  31prm  44730  127prm  44732  m11nprm  44734  lighneallem2  44739  lighneallem3  44740  3exp4mod41  44749  41prothprmlem1  44750  41prothprmlem2  44751  41prothprm  44752  m1expevenALTV  44780  1oddALTV  44823  6even  44844  8even  44846  2exp340mod341  44866  341fppr2  44867  4fppr1  44868  8exp8mod9  44869  9fppr8  44870  nfermltl8rev  44875  gbpart7  44900  gbpart9  44902  gbpart11  44903  sbgoldbo  44920  bgoldbtbndlem1  44938  tgoldbachlt  44949  subsubmgm  45032  altgsumbcALT  45370  lincfsuppcl  45435  linccl  45436  lincvalsn  45439  lincdifsn  45446  lincsum  45451  lincscm  45452  lindslinindimp2lem4  45483  lindslinindsimp2lem5  45484  snlindsntor  45493  lincresunit3lem2  45502  zlmodzxzldeplem3  45524  ldepsnlinc  45530  nn0sumshdiglemA  45646  nn0sumshdiglemB  45647  ackval2  45709  ackval2012  45718  ackval3012  45719  ackval41a  45721  ackval42  45723  ackval42a  45724  affinecomb1  45729  rrx2linest  45769  itschlc0yqe  45787  itsclc0yqsollem1  45789  itscnhlc0xyqsol  45792  itschlc0xyqsol1  45793  itsclquadb  45803  2itscplem2  45806  itscnhlinecirc02plem2  45810  sinh-conventional  46120  onetansqsecsq  46142  cotsqcscsq  46143  mvlraddi  46153  mvrladdi  46154  mvlrmuli  46160  amgmwlem  46185  amgmlemALT  46186
  Copyright terms: Public domain W3C validator