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

Theorem oveq1i 6537
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 6534 . 2 (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
31, 2ax-mp 5 1 (𝐴𝐹𝐶) = (𝐵𝐹𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  (class class class)co 6527
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-iota 5754  df-fv 5798  df-ov 6530
This theorem is referenced by:  caov12  6737  caov411  6741  omopthlem1  7599  map1  7898  pw2eng  7928  fsuppunbi  8156  cnfcomlem  8456  cnfcom2  8459  infxpenc2  8705  adderpqlem  9632  addassnq  9636  distrnq  9639  halfnq  9654  archnq  9658  addclprlem2  9695  addcmpblnr  9746  ltsrpr  9754  m1m1sr  9770  recexsrlem  9780  sqgt0sr  9783  map2psrpr  9787  axi2m1  9836  axcnre  9841  mul02lem2  10064  addid1  10067  cnegex2  10069  addid2  10070  mvrraddi  10149  mvlladdi  10150  negsubdi  10188  mulneg1  10317  recextlem1  10506  recdiv  10580  divmul13i  10635  mvllmuli  10707  2p2e4  10991  2times  10992  3p2e5  11007  3p3e6  11008  4p2e6  11009  4p3e7  11010  4p4e8  11011  5p2e7  11012  5p3e8  11013  5p4e9  11014  5p5e10OLD  11015  6p2e8  11016  6p3e9  11017  6p4e10OLD  11018  7p2e9  11019  7p3e10OLD  11020  8p2e10OLD  11021  1mhlfehlf  11098  8th4div3  11099  halfpm6th  11100  nneo  11293  dfdecOLD  11327  9p1e10  11328  dfdec10  11329  num0h  11341  numsuc  11343  dec10p  11385  dec10pOLD  11386  numma  11389  nummac  11390  numma2c  11391  numadd  11392  numaddc  11393  nummul2c  11395  decaddci  11412  decsubi  11415  decsubiOLD  11416  decmul1  11417  decmul1OLD  11418  5p5e10  11428  6p4e10  11430  7p3e10  11435  8p2e10  11442  decbin0  11514  decbin2  11515  xmulm1  11940  xadddi2  11956  x2times  11958  elfzp1b  12241  elfzm1b  12242  fz0to4untppr  12266  fz0sn0fz1  12280  fz1fzo0m1  12338  fldiv4p1lem1div2  12453  quoremz  12471  quoremnn0ALT  12473  uzrdgxfr  12583  mulexpz  12717  expaddz  12721  sqrecii  12763  sq4e2t8  12779  cu2  12780  i3  12783  iexpcyc  12786  binom2i  12791  binom3  12802  crreczi  12806  discr  12818  3dec  12867  sq10OLD  12868  3decOLD  12870  nn0opthlem1  12872  nn0opth2i  12875  faclbnd  12894  bcm1k  12919  bcp1nk  12921  bcpasc  12925  hashp1i  13004  hashxplem  13032  hashpw  13035  hashfun  13036  hashbc  13046  ccatlid  13168  swrdccatin12  13288  revs1  13311  cats1cat  13403  cats2cat  13404  lsws2  13445  lsws3  13446  lsws4  13447  s3s4  13474  s2s5  13475  s5s2  13476  imre  13642  crim  13649  remullem  13662  cnpart  13774  sqrtneglem  13801  absexpz  13839  absimle  13843  sqreulem  13893  amgm2  13903  iseraltlem2  14207  iseraltlem3  14208  modfsummod  14313  binomlem  14346  binom11  14349  arisum  14377  arisum2  14378  georeclim  14388  geo2sum  14389  mertenslem1  14401  mertens  14403  prodfrec  14412  fprodm1s  14485  fprodp1s  14486  fprodmodd  14513  fallfacfwd  14552  0risefac  14554  bpolydiflem  14570  bpoly2  14573  bpoly3  14574  bpoly4  14575  fsumcube  14576  efzval  14617  resinval  14650  recosval  14651  efi4p  14652  tan0  14666  efival  14667  sinhval  14669  coshval  14670  cosadd  14680  cos2tsin  14694  ef01bndlem  14699  cos1bnd  14702  cos2bnd  14703  absefib  14713  efieq1re  14714  demoivreALT  14716  eirrlem  14717  rpnnen2lem3  14730  rpnnen2lem11  14738  ruclem7  14750  3dvds  14836  3dvdsOLD  14837  3dvdsdec  14838  3dvdsdecOLD  14839  3dvds2dec  14840  3dvds2decOLD  14841  odd2np1  14849  nn0o1gt2  14881  nn0o  14883  pwp1fsum  14898  divalglem2  14902  divalglem9  14908  flodddiv4  14921  m1bits  14946  sadcp1  14961  sadeq  14978  smupp1  14986  smumul  14999  gcdaddmlem  15029  3lcm2e6woprm  15112  nn0gcdsq  15244  phiprmpw  15265  prmdiv  15274  prmdiveq  15275  prmdivdiv  15276  pythagtriplem1  15305  pythagtriplem12  15315  pythagtriplem14  15317  pockthi  15395  infpnlem1  15398  prmreclem4  15407  4sqlem12  15444  4sqlem13  15445  4sqlem19  15451  vdwapun  15462  vdwlem6  15474  0hashbc  15495  prmo2  15528  prmo3  15529  dec5dvds  15552  dec5nprm  15554  dec2nprm  15555  modxai  15556  modxp1i  15558  mod2xnegi  15559  modsubi  15560  gcdmodi  15562  decexp2  15563  decsplit0b  15568  decsplit1  15570  decsplit  15571  decsplit0bOLD  15572  decsplit1OLD  15574  decsplitOLD  15575  karatsuba  15576  karatsubaOLD  15577  2exp8  15580  3exp3  15582  5prm  15599  7prm  15601  11prm  15606  prmlem2  15611  37prm  15612  43prm  15613  83prm  15614  139prm  15615  163prm  15616  317prm  15617  631prm  15618  prmo5  15620  1259lem1  15622  1259lem2  15623  1259lem3  15624  1259lem4  15625  1259lem5  15626  1259prm  15627  2503lem1  15628  2503lem2  15629  2503lem3  15630  2503prm  15631  4001lem1  15632  4001lem2  15633  4001lem3  15634  4001lem4  15635  4001prm  15636  pwsbas  15916  rcaninv  16223  subsubc  16282  xpccatid  16597  subsubm  17126  mulg2  17319  subsubg  17386  oppgmnd  17553  gsumwrev  17565  psgnunilem2  17684  sylow1lem1  17782  subgslw  17800  sylow3  17817  efginvrel2  17909  efgsfo  17921  frgpnabllem1  18045  gsumzaddlem  18090  gsummptfzsplitl  18102  gsummpt1n0  18133  dprdfid  18185  ablfac1lem  18236  pgpfac1lem3  18245  pgpfaclem1  18249  mgpress  18269  srgbinomlem4  18312  opprring  18400  unitsubm  18439  subsubrg  18575  lsslss  18728  evlsval  19286  mpff  19300  coe1fzgsumdlem  19438  evl1gsumdlem  19487  xrsnsgrp  19547  gzrngunit  19577  expghm  19608  chrid  19639  zrhpsgnmhm  19694  psgndiflemA  19711  frlmip  19878  frlmphl  19881  matvsca2  19995  mattposvs  20022  m2detleiblem3  20196  m2detleiblem4  20197  cpmidpmat  20439  resstopn  20742  cnmpt1res  21231  ressuss  21819  iscusp2  21858  ucnextcn  21860  txmetcnp  22103  rerest  22347  xrtgioo  22349  xrrest  22350  cnmpt2pc  22466  xrhmeo  22484  clmvs2  22633  clmnegneg  22643  ncvsm1  22688  ncvspi  22690  reust  22894  rrxprds  22902  csbren  22907  minveclem2  22922  ovolunlem1a  22988  ovolicc2lem4  23012  uniioombllem5  23078  iblabs  23318  iblabsr  23319  iblmulc2  23320  itgmulc2  23323  limcres  23373  dvfval  23384  dvreslem  23396  dvres2lem  23397  dvcnp2  23406  cpnres  23423  dvcobr  23432  dveflem  23463  lhop1lem  23497  lhop2  23499  dvcnvrelem2  23502  plyun0  23674  coeeulem  23701  coeeu  23702  dvply1  23760  dvtaylp  23845  taylthlem2  23849  taylth  23850  dvradcnv  23896  pserdvlem2  23903  abelthlem8  23914  abelth  23916  sinhalfpilem  23936  cospi  23945  eulerid  23947  cos2pi  23949  ef2kpi  23951  sinhalfpip  23965  sinhalfpim  23966  coshalfpip  23967  coshalfpim  23968  sincosq3sgn  23973  sincosq4sgn  23974  tangtx  23978  sincos4thpi  23986  sincos6thpi  23988  sineq0  23994  tanregt0  24006  logm1  24056  abslogle  24085  tanarg  24086  logcnlem4  24108  advlogexp  24118  cxpsqrt  24166  dvsqrt  24200  dvcnsqrt  24202  cxpcn3  24206  root1cj  24214  cxpeq  24215  logb1  24224  ang180lem1  24256  ang180lem2  24257  ang180lem3  24258  lawcos  24263  isosctrlem1  24265  isosctrlem2  24266  quad2  24283  1cubrlem  24285  1cubr  24286  dcubic1lem  24287  dcubic2  24288  mcubic  24291  binom4  24294  dquartlem1  24295  quart1lem  24299  quart1  24300  quartlem1  24301  asinlem  24312  asinlem2  24313  asinlem3a  24314  acosneg  24331  efiasin  24332  asinsinlem  24335  asinsin  24336  acoscos  24337  asin1  24338  acosbnd  24344  atancj  24354  efiatan  24356  atanlogaddlem  24357  efiatan2  24361  2efiatan  24362  tanatan  24363  cosatan  24365  atantan  24367  atanbndlem  24369  atans2  24375  dvatan  24379  atantayl  24381  atantayl2  24382  log2cnv  24388  log2tlbnd  24389  log2ublem2  24391  log2ublem3  24392  log2ub  24393  birthday  24398  jensenlem1  24430  amgmlem  24433  lgamgulmlem2  24473  lgamgulmlem5  24476  lgambdd  24480  wilthlem1  24511  ftalem2  24517  ftalem5  24520  ftalem6  24521  basellem2  24525  basellem3  24526  basellem5  24528  basellem8  24531  basellem9  24532  mule1  24591  ppi1i  24611  musum  24634  ppiublem1  24644  ppiublem2  24645  ppiub  24646  chtublem  24653  chtub  24654  dchrptlem1  24706  dchrptlem2  24707  bclbnd  24722  bposlem6  24731  bposlem8  24733  bposlem9  24734  lgslem4  24742  lgsdir2lem1  24767  lgsdir2lem2  24768  lgsdir2lem4  24770  lgsdir2lem5  24771  lgsne0  24777  1lgs  24782  gausslemma2dlem0e  24802  gausslemma2dlem0f  24803  gausslemma2dlem3  24810  gausslemma2d  24816  lgseisenlem1  24817  lgseisenlem2  24818  lgseisenlem3  24819  lgseisenlem4  24820  lgseisen  24821  lgsquadlem1  24822  lgsquadlem2  24823  lgsquad2lem1  24826  lgsquad2lem2  24827  m1lgs  24830  2lgslem3a  24838  2lgslem3b  24839  2lgslem3c  24840  2lgslem3d  24841  2lgsoddprmlem3a  24852  2lgsoddprmlem3b  24853  2lgsoddprmlem3c  24854  2lgsoddprmlem3d  24855  chebbnd1lem2  24876  chebbnd1lem3  24877  rplogsumlem2  24891  dchrisum0flblem1  24914  dchrisum0re  24919  mulog2sumlem2  24941  chpdifbndlem1  24959  pntpbnd1a  24991  pntpbnd2  24993  pntibndlem2  24997  pntibndlem3  24998  pntlemg  25004  pntlemk  25012  pntlemo  25013  axsegconlem1  25515  ax5seglem7  25533  axlowdimlem3  25542  axlowdimlem16  25555  axlowdimlem17  25556  fargshiftlem  25928  constr3trllem3  25946  eupares  26268  konigsberg  26280  numclwwlk5  26405  numclwwlk7  26407  frgraregord013  26411  ex-fl  26462  ex-mod  26464  ex-exp  26465  ex-bc  26467  ex-lcm  26473  ex-ind-dvds  26476  vc2OLD  26576  vc0  26590  vcm  26592  vcnegnegOLD  26595  nvnncan  26688  nvm1  26697  nvpi  26699  nvmtri  26704  nvge0  26707  ipval3  26749  ipidsq  26753  ip0i  26870  ip1ilem  26871  ip2i  26873  ipdirilem  26874  ipasslem10  26884  siilem1  26896  siii  26898  minvecolem2  26921  hvsubid  27073  hvaddsubval  27080  hvmul2negi  27095  hvadd12i  27104  hv2times  27108  hvnegdii  27109  hvaddcani  27112  hi01  27143  hisubcomi  27151  normlem0  27156  normlem1  27157  normlem3  27159  normlem9  27165  bcseqi  27167  normsqi  27179  norm-ii-i  27184  normsubi  27188  norm3difi  27194  norm3adifii  27195  normpar2i  27203  polid2i  27204  polidi  27205  chdmm2i  27527  chj12i  27571  spanunsni  27628  qlaxr5i  27684  osumcor2i  27693  spansnji  27695  pjadjii  27723  pjinormii  27725  pjsslem  27728  pjpythi  27771  mayete3i  27777  mayetes3i  27778  hoadd12i  27826  honegneg  27855  ho2times  27868  hoaddsubi  27870  hosd1i  27871  hosd2i  27872  honpncani  27876  lnopeq0lem1  28054  lnopunilem1  28059  lnophmlem2  28066  lnfn0i  28091  nmopcoadji  28150  nmopcoadj2i  28151  opsqrlem1  28189  opsqrlem5  28193  opsqrlem6  28194  pjclem3  28246  stadd3i  28297  mddmd2  28358  mdexchi  28384  cvexchlem  28417  atomli  28431  atordi  28433  atabs2i  28451  mdsymlem1  28452  iuninc  28567  suppss2f  28625  suppss3  28696  archirngz  28880  gsumvsca2  28920  nn0omnd  28978  nn0archi  28980  xrge0slmod  28981  lmatfvlem  29015  sqsscirc1  29088  cnvordtrestixx  29093  raddcn  29109  xrge0iifhom  29117  xrge0mulc1cn  29121  xrge0tmd  29126  lmlimxrge0  29128  qqhucn  29170  rrhcn  29175  qqtopn  29189  rrhqima  29192  brfae  29444  inelcarsg  29506  cndprobnul  29632  isrrvv  29638  ballotlem1  29681  ballotlem2  29683  ballotlemodife  29692  ballotlemi1  29697  ballotlemii  29698  ballotlemic  29701  ballotlem1c  29702  ballotlemfrceq  29723  ballotth  29732  ofcs2  29754  signsvtn0  29779  signstfveq0  29786  signsvtp  29792  signsvtn  29793  signsvfpn  29794  signsvfnn  29795  signshf  29797  subfacp1lem1  30221  subfacp1lem5  30226  subfacp1lem6  30227  subfaclim  30230  cvmliftlem5  30331  cvmliftlem8  30334  cvmliftlem10  30336  cvmliftlem13  30338  cvmlift2lem6  30350  cvmlift2lem12  30356  problem1  30618  problem2  30619  problem2OLD  30620  problem4  30622  quad3  30624  iexpire  30680  sin2h  32365  poimirlem16  32391  poimirlem17  32392  poimirlem18  32393  poimirlem19  32394  poimirlem20  32395  poimirlem21  32396  poimirlem22  32397  poimirlem26  32401  mblfinlem3  32414  ismblfin  32416  itg2addnclem3  32429  iblabsnc  32440  iblmulc2nc  32441  itgmulc2nc  32444  ftc1cnnc  32450  ftc1anclem6  32456  ftc1anclem7  32457  ftc1anclem8  32458  dvasin  32462  fdc  32507  heiborlem4  32579  heiborlem6  32581  dalem24  33797  pmod2iN  33949  cdleme9  34354  cdleme20aN  34411  cdleme22e  34446  cdleme22eALTN  34447  cdleme25cv  34460  cdleme29b  34477  cdlemh1  34917  cdlemh2  34918  cdlemk35  35014  cdlemkid1  35024  pellexlem5  36211  reglog1  36274  jm2.23  36377  jm2.27c  36388  lnmlsslnm  36465  lmhmlnmsplit  36471  cntzsdrg  36587  areaquad  36617  cotrclrcl  36849  inductionexd  37269  hashnzfz2  37338  lhe4.4ex1a  37346  binomcxplemdvsum  37372  binomcxplemnotnn0  37373  binomcxp  37374  sineq0ALT  37991  unirnmapsn  38197  fzisoeu  38251  fz1ssfz0  38261  fsummulc1f  38432  fprodexp  38458  constlimc  38488  sumnnodd  38494  limcresiooub  38506  limcresioolb  38507  cncfshiftioo  38575  fperdvper  38605  dvnmul  38630  dvmptfprod  38632  itgsinexplem1  38642  stoweidlem11  38701  stoweidlem13  38703  stoweidlem26  38716  stoweidlem34  38724  wallispilem4  38758  wallispi2lem1  38761  wallispi2lem2  38762  stirlinglem11  38774  dirkerper  38786  dirkertrigeqlem1  38788  dirkertrigeqlem3  38790  dirkercncflem1  38793  dirkercncflem4  38796  fourierdlem30  38827  fourierdlem32  38829  fourierdlem33  38830  fourierdlem42  38839  fourierdlem46  38842  fourierdlem47  38843  fourierdlem57  38853  fourierdlem60  38856  fourierdlem61  38857  fourierdlem62  38858  fourierdlem68  38864  fourierdlem73  38869  fourierdlem79  38875  fourierdlem89  38885  fourierdlem90  38886  fourierdlem91  38887  fourierdlem96  38892  fourierdlem97  38893  fourierdlem98  38894  fourierdlem99  38895  fourierdlem100  38896  fourierdlem103  38899  fourierdlem104  38900  fourierdlem108  38904  fourierdlem110  38906  fourierdlem113  38909  sqwvfoura  38918  sqwvfourb  38919  fourierswlem  38920  fouriersw  38921  fouriercn  38922  etransclem4  38928  etransclem7  38931  etransclem23  38947  etransclem24  38948  etransclem25  38949  etransclem26  38950  etransclem31  38955  etransclem32  38956  etransclem35  38959  etransclem37  38961  etransclem46  38970  rrxdsfi  38978  rrndistlt  38983  sge0tsms  39070  sge0xaddlem2  39124  vonioolem2  39369  1t10e1p1e11  39735  1t10e1p1e11OLD  39736  deccarry  39739  1fzopredsuc  39745  m1mod0mod1  39747  iccpartgt  39763  fmtno0  39788  fmtno1  39789  fmtnorec2  39791  fmtno2  39798  fmtno3  39799  fmtno4  39800  fmtno5  39805  257prm  39809  fmtnofac1  39818  fmtno4prmfac  39820  fmtno4prmfac193  39821  fmtno4nprmfac193  39822  pwdif  39837  m2prm  39841  m3prm  39842  flsqrt5  39845  3ndvds4  39846  139prmALT  39847  31prm  39848  2exp7  39850  127prm  39851  m11nprm  39854  lighneallem2  39859  lighneallem3  39860  3exp4mod41  39869  41prothprmlem1  39870  41prothprmlem2  39871  41prothprm  39872  m1expevenALTV  39896  1oddALTV  39937  6even  39956  8even  39958  gbpart7  39987  gbpart9  39989  gbpart11  39990  bgoldbtbndlem1  40019  tgoldbachlt  40028  tgoldbachltOLD  40035  pfxccatin12  40086  elfz0lmr  40187  vdegp1bi-av  40748  1wlkp1lem1  40877  sPthisPth  40927  21wlkdlem1  41127  2pthd  41142  31wlkdlem1  41321  3pthd  41336  eucrct2eupth  41408  av-numclwwlk5  41537  av-numclwwlk7  41540  av-frgraregord013  41544  subsubmgm  41582  altgsumbcALT  41919  lincfsuppcl  41991  linccl  41992  lincvalsn  41995  lincdifsn  42002  lincsum  42007  lincscm  42008  lindslinindimp2lem4  42039  lindslinindsimp2lem5  42040  snlindsntor  42049  lincresunit3lem2  42058  zlmodzxzldeplem3  42080  ldepsnlinc  42086  nn0sumshdiglemA  42206  nn0sumshdiglemB  42207  sinh-conventional  42235  onetansqsecsq  42257  cotsqcscsq  42258  dpfrac1  42268  dpfrac1OLD  42269  mvlraddi  42279  mvrladdi  42281  mvlrmuli  42288  amgmwlem  42313  amgmlemALT  42314
  Copyright terms: Public domain W3C validator