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

Theorem oveq1i 6315
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 6312 . 2  |-  ( A  =  B  ->  ( A F C )  =  ( B F C ) )
31, 2ax-mp 5 1  |-  ( A F C )  =  ( B F C )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437  (class class class)co 6305
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rex 2788  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-iota 5565  df-fv 5609  df-ov 6308
This theorem is referenced by:  caov12  6511  caov411  6515  omopthlem1  7364  map1  7655  pw2eng  7684  fsuppunbi  7910  cnfcomlem  8203  cnfcom2  8206  infxpenc2  8451  adderpqlem  9378  addassnq  9382  distrnq  9385  halfnq  9400  archnq  9404  addclprlem2  9441  addcmpblnr  9492  ltsrpr  9500  m1m1sr  9516  recexsrlem  9526  sqgt0sr  9529  map2psrpr  9533  axi2m1  9582  axcnre  9587  mul02lem2  9809  addid1  9812  cnegex2  9814  addid2  9815  mvlladdi  9891  negsubdi  9929  mulneg1  10054  recextlem1  10241  recdiv  10312  divmul13i  10367  mvllmuli  10439  2p2e4  10727  2times  10728  3p2e5  10742  3p3e6  10743  4p2e6  10744  4p3e7  10745  4p4e8  10746  5p2e7  10747  5p3e8  10748  5p4e9  10749  5p5e10  10750  6p2e8  10751  6p3e9  10752  6p4e10  10753  7p2e9  10754  7p3e10  10755  8p2e10  10756  1mhlfehlf  10832  8th4div3  10833  halfpm6th  10834  nneo  11019  num0h  11061  numsuc  11063  dec10p  11080  numma  11082  nummac  11083  numma2c  11084  numadd  11085  numaddc  11086  nummul2c  11088  decaddci  11096  decbin0  11154  decbin2  11155  xmulm1  11567  xadddi2  11583  x2times  11585  elfzp1b  11869  elfzm1b  11870  quoremz  12079  quoremnn0ALT  12081  uzrdgxfr  12177  mulexpz  12309  expaddz  12313  sqrecii  12354  cu2  12370  i3  12373  iexpcyc  12376  binom2i  12381  binom3  12390  crreczi  12394  discr  12406  nn0opthlem1  12451  nn0opth2i  12454  faclbnd  12472  bcm1k  12497  bcp1nk  12499  bcpasc  12503  hashp1i  12577  hashxplem  12600  hashpw  12603  hashfun  12604  hashbc  12611  ccatlid  12717  swrdccatin12  12832  revs1  12855  cats1cat  12942  imre  13150  crim  13157  remullem  13170  cnpart  13282  sqrtneglem  13309  absexpz  13347  absimle  13351  sqreulem  13401  amgm2  13411  iseraltlem2  13727  iseraltlem3  13728  modfsummod  13832  binomlem  13865  binom11  13868  arisum  13896  arisum2  13897  georeclim  13906  geo2sum  13907  mertenslem1  13918  mertens  13920  prodfrec  13929  fprodm1s  14002  fprodp1s  14003  fallfacfwd  14067  0risefac  14069  bpolydiflem  14085  bpoly2  14088  bpoly3  14089  bpoly4  14090  fsumcube  14091  efzval  14134  resinval  14167  recosval  14168  efi4p  14169  tan0  14183  efival  14184  sinhval  14186  coshval  14187  cosadd  14197  cos2tsin  14211  ef01bndlem  14216  cos1bnd  14219  cos2bnd  14220  absefib  14230  efieq1re  14231  demoivreALT  14233  eirrlem  14234  rpnnen2lem3  14247  rpnnen2lem11  14255  ruclem7  14266  odd2np1  14343  3dvds  14347  divalglem2  14351  divalglem9  14357  m1bits  14388  sadcp1  14403  sadeq  14420  smupp1  14428  smumul  14441  gcdaddmlem  14466  3lcm2e6woprm  14545  nn0gcdsq  14663  phiprmpw  14684  prmdiv  14693  prmdiveq  14694  prmdivdiv  14695  pythagtriplem1  14720  pythagtriplem12  14730  pythagtriplem14  14732  pockthi  14805  infpnlem1  14808  prmreclem4  14817  4sqlem12  14854  4sqlem13OLD  14855  4sqlem13  14861  4sqlem19  14867  vdwapun  14878  vdwlem6  14890  0hashbc  14913  prmo2  14952  prmo3  14953  dec5dvds  14990  dec5nprm  14992  dec2nprm  14993  modxai  14994  modxp1i  14996  mod2xnegi  14997  modsubi  14998  gcdmodi  15000  decexp2  15001  decsplit0b  15006  decsplit1  15008  decsplit  15009  karatsuba  15010  2exp6OLD  15013  2exp8  15014  3exp3  15016  5prm  15034  7prm  15036  11prm  15040  prmlem2  15045  37prm  15046  43prm  15047  83prm  15048  139prm  15049  163prm  15050  317prm  15051  631prm  15052  prmo5  15054  1259lem1  15056  1259lem2  15057  1259lem3  15058  1259lem4  15059  1259lem5  15060  1259prm  15061  2503lem1  15062  2503lem2  15063  2503lem3  15064  2503prm  15065  4001lem1  15066  4001lem2  15067  4001lem3  15068  4001lem4  15069  4001prm  15070  pwsbas  15335  rcaninv  15641  subsubc  15700  xpccatid  16015  subsubm  16546  mulg2  16709  subsubg  16782  oppgmnd  16947  gsumwrev  16959  psgnunilem2  17078  sylow1lem1  17176  subgslw  17194  sylow3  17211  efginvrel2  17303  efgsfo  17315  frgpnabllem1  17435  gsumzaddlem  17480  gsummptfzsplitl  17492  gsummpt1n0  17523  dprdfid  17576  ablfac1lem  17627  pgpfac1lem3  17636  pgpfaclem1  17640  mgpress  17660  srgbinomlem4  17702  opprring  17785  unitsubm  17824  subsubrg  17960  lsslss  18110  evlsval  18668  mpff  18682  coe1fzgsumdlem  18821  evl1gsumdlem  18870  xrsnsgrp  18930  gzrngunit  18959  expghm  18989  chrid  19020  zrhpsgnmhm  19074  psgndiflemA  19091  frlmip  19258  frlmphl  19261  matvsca2  19375  mattposvs  19402  m2detleiblem3  19576  m2detleiblem4  19577  cpmidpmat  19819  resstopn  20124  cnmpt1res  20613  ressuss  21200  iscusp2  21239  ucnextcn  21241  txmetcnp  21484  rerest  21724  xrtgioo  21726  xrrest  21727  cnmpt2pc  21843  xrhmeo  21861  reust  22224  rrxprds  22232  csbren  22237  minveclem2  22252  ovolunlem1a  22318  ovolicc2lem4  22342  uniioombllem5  22413  iblabs  22654  iblabsr  22655  iblmulc2  22656  itgmulc2  22659  limcres  22709  dvfval  22720  dvreslem  22732  dvres2lem  22733  dvcnp2  22742  cpnres  22759  dvcobr  22768  dveflem  22799  lhop1lem  22833  lhop2  22835  dvcnvrelem2  22838  plyun0  23010  coeeulem  23037  coeeu  23038  dvply1  23096  dvtaylp  23181  taylthlem2  23185  taylth  23186  dvradcnv  23232  pserdvlem2  23239  abelthlem8  23250  abelth  23252  sinhalfpilem  23274  cospi  23283  eulerid  23285  cos2pi  23287  ef2kpi  23289  sinhalfpip  23303  sinhalfpim  23304  coshalfpip  23305  coshalfpim  23306  sincosq3sgn  23311  sincosq4sgn  23312  tangtx  23316  sincos4thpi  23324  sincos6thpi  23326  sineq0  23332  tanregt0  23344  logm1  23394  abslogle  23423  tanarg  23424  logcnlem4  23446  advlogexp  23456  cxpsqrt  23504  dvsqrt  23538  dvcnsqrt  23540  cxpcn3  23544  root1cj  23552  cxpeq  23553  logb1  23562  ang180lem1  23594  ang180lem2  23595  ang180lem3  23596  lawcos  23601  isosctrlem1  23603  isosctrlem2  23604  quad2  23621  1cubrlem  23623  1cubr  23624  dcubic1lem  23625  dcubic2  23626  mcubic  23629  binom4  23632  dquartlem1  23633  quart1lem  23637  quart1  23638  quartlem1  23639  asinlem  23650  asinlem2  23651  asinlem3a  23652  acosneg  23669  efiasin  23670  asinsinlem  23673  asinsin  23674  acoscos  23675  asin1  23676  acosbnd  23682  atancj  23692  efiatan  23694  atanlogaddlem  23695  efiatan2  23699  2efiatan  23700  tanatan  23701  cosatan  23703  atantan  23705  atanbndlem  23707  atans2  23713  dvatan  23717  atantayl  23719  atantayl2  23720  log2cnv  23726  log2tlbnd  23727  log2ublem2  23729  log2ublem3  23730  log2ub  23731  birthday  23736  jensenlem1  23768  amgmlem  23771  lgamgulmlem2  23811  lgamgulmlem5  23814  lgambdd  23818  wilthlem1  23849  ftalem2  23854  ftalem5  23857  ftalem6  23858  basellem2  23862  basellem3  23863  basellem5  23865  basellem8  23868  basellem9  23869  mule1  23929  ppi1i  23949  musum  23974  ppiublem1  23984  ppiublem2  23985  ppiub  23986  chtublem  23993  chtub  23994  dchrptlem1  24046  dchrptlem2  24047  bclbnd  24062  bpos1  24065  bposlem6  24071  bposlem8  24073  bposlem9  24074  lgslem4  24081  lgsdir2lem1  24105  lgsdir2lem2  24106  lgsdir2lem4  24108  lgsdir2lem5  24109  lgsne0  24115  1lgs  24119  lgseisenlem1  24131  lgseisenlem2  24132  lgseisenlem3  24133  lgseisenlem4  24134  lgseisen  24135  lgsquadlem1  24136  lgsquadlem2  24137  lgsquad2lem1  24140  lgsquad2lem2  24141  m1lgs  24144  chebbnd1lem2  24162  chebbnd1lem3  24163  rplogsumlem2  24177  dchrisum0flblem1  24200  dchrisum0re  24205  mulog2sumlem2  24227  chpdifbndlem1  24245  pntpbnd1a  24277  pntpbnd2  24279  pntibndlem2  24283  pntibndlem3  24284  pntlemg  24290  pntlemk  24298  pntlemo  24299  axsegconlem1  24784  ax5seglem7  24802  axlowdimlem3  24811  axlowdimlem16  24824  axlowdimlem17  24825  usgraexvlem  24959  fargshiftlem  25198  constr3trllem3  25216  eupares  25539  konigsberg  25551  numclwwlk5  25676  numclwwlk7  25678  frgraregord013  25682  ex-fl  25733  ex-ind-dvds  25735  addinv  25916  vc2  26010  vc0  26024  vcm  26026  vcnegneg  26029  nvnncan  26120  nvm1  26129  nvpi  26131  nvmtri  26136  nvge0  26139  ipval3  26181  ipidsq  26185  ip0i  26302  ip1ilem  26303  ip2i  26305  ipdirilem  26306  ipasslem10  26316  siilem1  26328  siii  26330  minvecolem2  26353  hvsubid  26505  hvaddsubval  26512  hvmul2negi  26527  hvadd12i  26536  hv2times  26540  hvnegdii  26541  hvaddcani  26544  hi01  26575  hisubcomi  26583  normlem0  26588  normlem1  26589  normlem3  26591  normlem9  26597  bcseqi  26599  normsqi  26611  norm-ii-i  26616  normsubi  26620  norm3difi  26626  norm3adifii  26627  normpar2i  26635  polid2i  26636  polidi  26637  chdmm2i  26957  chj12i  27001  spanunsni  27058  qlaxr5i  27114  osumcor2i  27123  spansnji  27125  pjadjii  27153  pjinormii  27155  pjsslem  27158  pjpythi  27201  mayete3i  27207  mayetes3i  27208  hoadd12i  27256  honegneg  27285  ho2times  27298  hoaddsubi  27300  hosd1i  27301  hosd2i  27302  honpncani  27306  lnopeq0lem1  27484  lnopunilem1  27489  lnophmlem2  27496  lnfn0i  27521  nmopcoadji  27580  nmopcoadj2i  27581  opsqrlem1  27619  opsqrlem5  27623  opsqrlem6  27624  pjclem3  27676  stadd3i  27727  mddmd2  27788  mdexchi  27814  cvexchlem  27847  atomli  27861  atordi  27863  atabs2i  27881  mdsymlem1  27882  iuninc  28006  suppss2f  28069  suppss3  28146  fz1fzo0m1  28206  archirngz  28335  gsumvsca2  28376  nn0omnd  28434  nn0archi  28436  xrge0slmod  28437  lmatfvlem  28471  sqsscirc1  28544  cnvordtrestixx  28549  raddcn  28565  xrge0iifhom  28573  xrge0mulc1cn  28577  xrge0tmd  28582  lmlimxrge0  28584  qqhucn  28626  rrhcn  28631  qqtopn  28645  rrhqima  28648  brfae  28901  inelcarsg  28963  cndprobnul  29087  isrrvv  29093  ballotlem1  29136  ballotlem2  29138  ballotlemodife  29147  ballotlemi1  29152  ballotlemii  29153  ballotlemic  29156  ballotlem1c  29157  ballotlemfrceq  29178  ballotth  29187  ofcs2  29213  signsvtn0  29238  signstfveq0  29245  signsvtp  29251  signsvtn  29252  signsvfpn  29253  signsvfnn  29254  signshf  29256  subfacp1lem1  29681  subfacp1lem5  29686  subfacp1lem6  29687  subfaclim  29690  cvmliftlem5  29791  cvmliftlem8  29794  cvmliftlem10  29796  cvmliftlem13  29798  cvmlift2lem6  29810  cvmlift2lem12  29816  problem1  30076  problem2  30077  problem4  30079  quad3  30081  iexpire  30149  sin2h  31629  poimirlem16  31650  poimirlem17  31651  poimirlem18  31652  poimirlem19  31653  poimirlem20  31654  poimirlem21  31655  poimirlem22  31656  poimirlem26  31660  mblfinlem3  31673  ismblfin  31675  itg2addnclem3  31689  iblabsnc  31700  iblmulc2nc  31701  itgmulc2nc  31704  ftc1cnnc  31710  ftc1anclem6  31716  ftc1anclem7  31717  ftc1anclem8  31718  dvasin  31722  fdc  31768  heiborlem4  31840  heiborlem6  31842  dalem24  32961  pmod2iN  33113  cdleme9  33518  cdleme20aN  33575  cdleme22e  33610  cdleme22eALTN  33611  cdleme25cv  33624  cdleme29b  33641  cdlemh1  34081  cdlemh2  34082  cdlemk35  34178  cdlemkid1  34188  pellexlem5  35377  reglog1  35440  jm2.23  35547  jm2.27c  35558  lnmlsslnm  35635  lmhmlnmsplit  35641  cntzsdrg  35757  areaquad  35790  cotrclrcl  35963  inductionexd  36220  hashnzfz2  36297  lhe4.4ex1a  36305  binomcxplemdvsum  36331  binomcxplemnotnn0  36332  binomcxp  36333  sineq0ALT  36964  fzisoeu  37117  fz1ssfz0  37127  fsummulc1f  37212  fprodexp  37236  constlimc  37266  sumnnodd  37272  limcresiooub  37285  limcresioolb  37286  cncfshiftioo  37332  fperdvper  37352  dvnmul  37377  dvmptfprod  37379  itgsinexplem1  37389  stoweidlem11  37430  stoweidlem13  37432  stoweidlem26  37445  stoweidlem34  37454  wallispilem4  37489  wallispi2lem1  37492  wallispi2lem2  37493  stirlinglem11  37505  dirkerper  37517  dirkertrigeqlem1  37519  dirkertrigeqlem3  37521  dirkercncflem1  37524  dirkercncflem4  37527  fourierdlem30  37558  fourierdlem32  37560  fourierdlem33  37561  fourierdlem42  37570  fourierdlem46  37574  fourierdlem47  37575  fourierdlem57  37585  fourierdlem60  37588  fourierdlem61  37589  fourierdlem62  37590  fourierdlem68  37596  fourierdlem73  37601  fourierdlem79  37607  fourierdlem89  37617  fourierdlem90  37618  fourierdlem91  37619  fourierdlem96  37624  fourierdlem97  37625  fourierdlem98  37626  fourierdlem99  37627  fourierdlem100  37628  fourierdlem103  37631  fourierdlem104  37632  fourierdlem108  37636  fourierdlem110  37638  fourierdlem113  37641  sqwvfoura  37650  sqwvfourb  37651  fourierswlem  37652  fouriersw  37653  fouriercn  37654  etransclem4  37660  etransclem7  37663  etransclem23  37679  etransclem24  37680  etransclem25  37681  etransclem26  37682  etransclem31  37687  etransclem32  37688  etransclem35  37691  etransclem37  37693  etransclem46  37702  sge0tsms  37746  1t10e1p1e11  38090  deccarry  38095  1fzopredsuc  38101  m1mod0mod1  38103  iccpartgt  38121  m1expevenALTV  38157  1oddALTV  38199  6even  38218  8even  38220  gbpart7  38248  gbpart9  38250  gbpart11  38251  bgoldbtbndlem1  38280  tgoldbachlt  38289  3exp4mod41  38296  41prothprmlem1  38297  41prothprmlem2  38298  41prothprm  38299  pfxccatin12  38346  subsubmgm  38545  altgsumbcALT  38884  lincfsuppcl  38956  linccl  38957  lincvalsn  38960  lincdifsn  38967  lincsum  38972  lincscm  38973  lindslinindimp2lem4  39004  lindslinindsimp2lem5  39005  snlindsntor  39014  lincresunit3lem2  39023  zlmodzxzldeplem3  39045  ldepsnlinc  39051  nn0o1gt2  39078  nn0o  39080  nn0sumshdiglemA  39181  nn0sumshdiglemB  39182  sinh-conventional  39210  onetansqsecsq  39232  cotsqcscsq  39233  dpfrac1  39243  mvlraddi  39255  mvrladdi  39257  mvrraddi  39259  mvlrmuli  39267
  Copyright terms: Public domain W3C validator