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

Theorem oveq1i 6254
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 6251 . 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 6244
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-rex 2715  df-rab 2718  df-v 3019  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-if 3850  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4158  df-br 4362  df-iota 5503  df-fv 5547  df-ov 6247
This theorem is referenced by:  caov12  6450  caov411  6454  omopthlem1  7306  map1  7597  pw2eng  7626  fsuppunbi  7852  cnfcomlem  8151  cnfcom2  8154  infxpenc2  8399  adderpqlem  9325  addassnq  9329  distrnq  9332  halfnq  9347  archnq  9351  addclprlem2  9388  addcmpblnr  9439  ltsrpr  9447  m1m1sr  9463  recexsrlem  9473  sqgt0sr  9476  map2psrpr  9480  axi2m1  9529  axcnre  9534  mul02lem2  9756  addid1  9759  cnegex2  9761  addid2  9762  mvlladdi  9838  negsubdi  9876  mulneg1  10001  recextlem1  10188  recdiv  10259  divmul13i  10314  mvllmuli  10386  2p2e4  10673  2times  10674  3p2e5  10688  3p3e6  10689  4p2e6  10690  4p3e7  10691  4p4e8  10692  5p2e7  10693  5p3e8  10694  5p4e9  10695  5p5e10  10696  6p2e8  10697  6p3e9  10698  6p4e10  10699  7p2e9  10700  7p3e10  10701  8p2e10  10702  1mhlfehlf  10778  8th4div3  10779  halfpm6th  10780  nneo  10965  num0h  11007  numsuc  11009  dec10p  11026  numma  11028  nummac  11029  numma2c  11030  numadd  11031  numaddc  11032  nummul2c  11034  decaddci  11042  decbin0  11100  decbin2  11101  xmulm1  11513  xadddi2  11529  x2times  11531  elfzp1b  11817  elfzm1b  11818  quoremz  12027  quoremnn0ALT  12029  uzrdgxfr  12125  mulexpz  12257  expaddz  12261  sqrecii  12302  cu2  12318  i3  12321  iexpcyc  12324  binom2i  12329  binom3  12338  crreczi  12342  discr  12354  nn0opthlem1  12399  nn0opth2i  12402  faclbnd  12420  bcm1k  12445  bcp1nk  12447  bcpasc  12451  hashp1i  12525  hashxplem  12548  hashpw  12551  hashfun  12552  hashbc  12559  ccatlid  12673  swrdccatin12  12788  revs1  12811  cats1cat  12898  imre  13110  crim  13117  remullem  13130  cnpart  13242  sqrtneglem  13269  absexpz  13307  absimle  13311  sqreulem  13361  amgm2  13371  iseraltlem2  13687  iseraltlem3  13688  modfsummod  13792  binomlem  13825  binom11  13828  arisum  13856  arisum2  13857  georeclim  13866  geo2sum  13867  mertenslem1  13878  mertens  13880  prodfrec  13889  fprodm1s  13962  fprodp1s  13963  fallfacfwd  14027  0risefac  14029  bpolydiflem  14045  bpoly2  14048  bpoly3  14049  bpoly4  14050  fsumcube  14051  efzval  14094  resinval  14127  recosval  14128  efi4p  14129  tan0  14143  efival  14144  sinhval  14146  coshval  14147  cosadd  14157  cos2tsin  14171  ef01bndlem  14176  cos1bnd  14179  cos2bnd  14180  absefib  14190  efieq1re  14191  demoivreALT  14193  eirrlem  14194  rpnnen2lem3  14207  rpnnen2lem11  14215  ruclem7  14226  odd2np1  14303  3dvds  14307  divalglem2  14311  divalglem2OLD  14312  divalglem9  14319  divalglem9OLD  14320  m1bits  14352  sadcp1  14367  sadeq  14384  smupp1  14392  smumul  14405  gcdaddmlem  14430  3lcm2e6woprm  14518  nn0gcdsq  14639  phiprmpw  14662  prmdiv  14671  prmdiveq  14672  prmdivdiv  14673  pythagtriplem1  14704  pythagtriplem12  14714  pythagtriplem14  14716  pockthi  14789  infpnlem1  14792  prmreclem4  14801  4sqlem12  14838  4sqlem13OLD  14839  4sqlem13  14845  4sqlem19  14851  vdwapun  14862  vdwlem6  14874  0hashbc  14897  prmo2  14936  prmo3  14937  dec5dvds  14974  dec5nprm  14976  dec2nprm  14977  modxai  14978  modxp1i  14980  mod2xnegi  14981  modsubi  14982  gcdmodi  14984  decexp2  14985  decsplit0b  14990  decsplit1  14992  decsplit  14993  karatsuba  14994  2exp6OLD  14997  2exp8  14998  3exp3  15000  5prm  15018  7prm  15020  11prm  15024  prmlem2  15029  37prm  15030  43prm  15031  83prm  15032  139prm  15033  163prm  15034  317prm  15035  631prm  15036  prmo5  15038  1259lem1  15040  1259lem2  15041  1259lem3  15042  1259lem4  15043  1259lem5  15044  1259prm  15045  2503lem1  15046  2503lem2  15047  2503lem3  15048  2503prm  15049  4001lem1  15050  4001lem2  15051  4001lem3  15052  4001lem4  15053  4001prm  15054  pwsbas  15323  rcaninv  15637  subsubc  15696  xpccatid  16011  subsubm  16542  mulg2  16705  subsubg  16778  oppgmnd  16943  gsumwrev  16955  psgnunilem2  17074  sylow1lem1  17188  subgslw  17206  sylow3  17223  efginvrel2  17315  efgsfo  17327  frgpnabllem1  17447  gsumzaddlem  17492  gsummptfzsplitl  17504  gsummpt1n0  17535  dprdfid  17588  ablfac1lem  17639  pgpfac1lem3  17648  pgpfaclem1  17652  mgpress  17672  srgbinomlem4  17714  opprring  17797  unitsubm  17836  subsubrg  17972  lsslss  18122  evlsval  18680  mpff  18694  coe1fzgsumdlem  18833  evl1gsumdlem  18882  xrsnsgrp  18942  gzrngunit  18971  expghm  19004  chrid  19035  zrhpsgnmhm  19089  psgndiflemA  19106  frlmip  19273  frlmphl  19276  matvsca2  19390  mattposvs  19417  m2detleiblem3  19591  m2detleiblem4  19592  cpmidpmat  19834  resstopn  20139  cnmpt1res  20628  ressuss  21215  iscusp2  21254  ucnextcn  21256  txmetcnp  21499  rerest  21759  xrtgioo  21761  xrrest  21762  cnmpt2pc  21893  xrhmeo  21911  reust  22277  rrxprds  22285  csbren  22290  minveclem2  22305  minveclem2OLD  22317  ovolunlem1a  22386  ovolicc2lem4OLD  22410  ovolicc2lem4  22411  uniioombllem5  22482  iblabs  22723  iblabsr  22724  iblmulc2  22725  itgmulc2  22728  limcres  22778  dvfval  22789  dvreslem  22801  dvres2lem  22802  dvcnp2  22811  cpnres  22828  dvcobr  22837  dveflem  22868  lhop1lem  22902  lhop2  22904  dvcnvrelem2  22907  plyun0  23088  coeeulem  23115  coeeu  23116  dvply1  23174  dvtaylp  23262  taylthlem2  23266  taylth  23267  dvradcnv  23313  pserdvlem2  23320  abelthlem8  23331  abelth  23333  sinhalfpilem  23355  cospi  23364  eulerid  23366  cos2pi  23368  ef2kpi  23370  sinhalfpip  23384  sinhalfpim  23385  coshalfpip  23386  coshalfpim  23387  sincosq3sgn  23392  sincosq4sgn  23393  tangtx  23397  sincos4thpi  23405  sincos6thpi  23407  sineq0  23413  tanregt0  23425  logm1  23475  abslogle  23504  tanarg  23505  logcnlem4  23527  advlogexp  23537  cxpsqrt  23585  dvsqrt  23619  dvcnsqrt  23621  cxpcn3  23625  root1cj  23633  cxpeq  23634  logb1  23643  ang180lem1  23675  ang180lem2  23676  ang180lem3  23677  lawcos  23682  isosctrlem1  23684  isosctrlem2  23685  quad2  23702  1cubrlem  23704  1cubr  23705  dcubic1lem  23706  dcubic2  23707  mcubic  23710  binom4  23713  dquartlem1  23714  quart1lem  23718  quart1  23719  quartlem1  23720  asinlem  23731  asinlem2  23732  asinlem3a  23733  acosneg  23750  efiasin  23751  asinsinlem  23754  asinsin  23755  acoscos  23756  asin1  23757  acosbnd  23763  atancj  23773  efiatan  23775  atanlogaddlem  23776  efiatan2  23780  2efiatan  23781  tanatan  23782  cosatan  23784  atantan  23786  atanbndlem  23788  atans2  23794  dvatan  23798  atantayl  23800  atantayl2  23801  log2cnv  23807  log2tlbnd  23808  log2ublem2  23810  log2ublem3  23811  log2ub  23812  birthday  23817  jensenlem1  23849  amgmlem  23852  lgamgulmlem2  23892  lgamgulmlem5  23895  lgambdd  23899  wilthlem1  23930  ftalem2  23935  ftalem5  23938  ftalem5OLD  23940  ftalem6  23941  basellem2  23945  basellem3  23946  basellem5  23948  basellem8  23951  basellem9  23952  mule1  24012  ppi1i  24032  musum  24057  ppiublem1  24067  ppiublem2  24068  ppiub  24069  chtublem  24076  chtub  24077  dchrptlem1  24129  dchrptlem2  24130  bclbnd  24145  bpos1  24148  bposlem6  24154  bposlem8  24156  bposlem9  24157  lgslem4  24164  lgsdir2lem1  24188  lgsdir2lem2  24189  lgsdir2lem4  24191  lgsdir2lem5  24192  lgsne0  24198  1lgs  24202  lgseisenlem1  24214  lgseisenlem2  24215  lgseisenlem3  24216  lgseisenlem4  24217  lgseisen  24218  lgsquadlem1  24219  lgsquadlem2  24220  lgsquad2lem1  24223  lgsquad2lem2  24224  m1lgs  24227  chebbnd1lem2  24245  chebbnd1lem3  24246  rplogsumlem2  24260  dchrisum0flblem1  24283  dchrisum0re  24288  mulog2sumlem2  24310  chpdifbndlem1  24328  pntpbnd1a  24360  pntpbnd2  24362  pntibndlem2  24366  pntibndlem3  24367  pntlemg  24373  pntlemk  24381  pntlemo  24382  axsegconlem1  24884  ax5seglem7  24902  axlowdimlem3  24911  axlowdimlem16  24924  axlowdimlem17  24925  usgraexmplvtxlem  25059  fargshiftlem  25299  constr3trllem3  25317  eupares  25640  konigsberg  25652  numclwwlk5  25777  numclwwlk7  25779  frgraregord013  25783  ex-fl  25834  ex-ind-dvds  25836  addinv  26017  vc2  26111  vc0  26125  vcm  26127  vcnegneg  26130  nvnncan  26221  nvm1  26230  nvpi  26232  nvmtri  26237  nvge0  26240  ipval3  26282  ipidsq  26286  ip0i  26403  ip1ilem  26404  ip2i  26406  ipdirilem  26407  ipasslem10  26417  siilem1  26429  siii  26431  minvecolem2  26454  minvecolem2OLD  26464  hvsubid  26616  hvaddsubval  26623  hvmul2negi  26638  hvadd12i  26647  hv2times  26651  hvnegdii  26652  hvaddcani  26655  hi01  26686  hisubcomi  26694  normlem0  26699  normlem1  26700  normlem3  26702  normlem9  26708  bcseqi  26710  normsqi  26722  norm-ii-i  26727  normsubi  26731  norm3difi  26737  norm3adifii  26738  normpar2i  26746  polid2i  26747  polidi  26748  chdmm2i  27068  chj12i  27112  spanunsni  27169  qlaxr5i  27225  osumcor2i  27234  spansnji  27236  pjadjii  27264  pjinormii  27266  pjsslem  27269  pjpythi  27312  mayete3i  27318  mayetes3i  27319  hoadd12i  27367  honegneg  27396  ho2times  27409  hoaddsubi  27411  hosd1i  27412  hosd2i  27413  honpncani  27417  lnopeq0lem1  27595  lnopunilem1  27600  lnophmlem2  27607  lnfn0i  27632  nmopcoadji  27691  nmopcoadj2i  27692  opsqrlem1  27730  opsqrlem5  27734  opsqrlem6  27735  pjclem3  27787  stadd3i  27838  mddmd2  27899  mdexchi  27925  cvexchlem  27958  atomli  27972  atordi  27974  atabs2i  27992  mdsymlem1  27993  iuninc  28117  suppss2f  28179  suppss3  28257  fz1fzo0m1  28324  archirngz  28452  gsumvsca2  28493  nn0omnd  28551  nn0archi  28553  xrge0slmod  28554  lmatfvlem  28588  sqsscirc1  28661  cnvordtrestixx  28666  raddcn  28682  xrge0iifhom  28690  xrge0mulc1cn  28694  xrge0tmd  28699  lmlimxrge0  28701  qqhucn  28743  rrhcn  28748  qqtopn  28762  rrhqima  28765  brfae  29018  inelcarsg  29090  cndprobnul  29217  isrrvv  29223  ballotlem1  29266  ballotlem2  29268  ballotlemodife  29277  ballotlemi1  29282  ballotlemii  29283  ballotlemic  29286  ballotlem1c  29287  ballotlemfrceq  29308  ballotth  29317  ballotlemi1OLD  29320  ballotlemiiOLD  29321  ballotlemicOLD  29324  ballotlem1cOLD  29325  ballotlemfrceqOLD  29346  ballotthOLD  29355  ofcs2  29381  signsvtn0  29406  signstfveq0  29413  signsvtp  29419  signsvtn  29420  signsvfpn  29421  signsvfnn  29422  signshf  29424  subfacp1lem1  29849  subfacp1lem5  29854  subfacp1lem6  29855  subfaclim  29858  cvmliftlem5  29959  cvmliftlem8  29962  cvmliftlem10  29964  cvmliftlem13  29966  cvmlift2lem6  29978  cvmlift2lem12  29984  problem1  30244  problem2  30245  problem4  30247  quad3  30249  iexpire  30317  sin2h  31842  poimirlem16  31863  poimirlem17  31864  poimirlem18  31865  poimirlem19  31866  poimirlem20  31867  poimirlem21  31868  poimirlem22  31869  poimirlem26  31873  mblfinlem3  31886  ismblfin  31888  itg2addnclem3  31902  iblabsnc  31913  iblmulc2nc  31914  itgmulc2nc  31917  ftc1cnnc  31923  ftc1anclem6  31929  ftc1anclem7  31930  ftc1anclem8  31931  dvasin  31935  fdc  31981  heiborlem4  32053  heiborlem6  32055  dalem24  33174  pmod2iN  33326  cdleme9  33731  cdleme20aN  33788  cdleme22e  33823  cdleme22eALTN  33824  cdleme25cv  33837  cdleme29b  33854  cdlemh1  34294  cdlemh2  34295  cdlemk35  34391  cdlemkid1  34401  pellexlem5  35590  reglog1  35657  jm2.23  35764  jm2.27c  35775  lnmlsslnm  35852  lmhmlnmsplit  35858  cntzsdrg  35981  areaquad  36014  cotrclrcl  36247  inductionexd  36506  hashnzfz2  36583  lhe4.4ex1a  36591  binomcxplemdvsum  36617  binomcxplemnotnn0  36618  binomcxp  36619  sineq0ALT  37250  fzisoeu  37415  fz1ssfz0  37425  fsummulc1f  37531  fprodexp  37557  constlimc  37587  sumnnodd  37593  limcresiooub  37606  limcresioolb  37607  cncfshiftioo  37653  fperdvper  37673  dvnmul  37701  dvmptfprod  37703  itgsinexplem1  37713  stoweidlem11  37754  stoweidlem13  37756  stoweidlem26  37769  stoweidlem34  37778  wallispilem4  37813  wallispi2lem1  37816  wallispi2lem2  37817  stirlinglem11  37829  dirkerper  37841  dirkertrigeqlem1  37843  dirkertrigeqlem3  37845  dirkercncflem1  37848  dirkercncflem4  37851  fourierdlem30  37882  fourierdlem32  37885  fourierdlem33  37886  fourierdlem42  37895  fourierdlem42OLD  37896  fourierdlem46  37899  fourierdlem47  37900  fourierdlem57  37910  fourierdlem60  37913  fourierdlem61  37914  fourierdlem62  37915  fourierdlem68  37921  fourierdlem73  37926  fourierdlem79  37932  fourierdlem89  37942  fourierdlem90  37943  fourierdlem91  37944  fourierdlem96  37949  fourierdlem97  37950  fourierdlem98  37951  fourierdlem99  37952  fourierdlem100  37953  fourierdlem103  37956  fourierdlem104  37957  fourierdlem108  37961  fourierdlem110  37963  fourierdlem113  37966  sqwvfoura  37975  sqwvfourb  37976  fourierswlem  37977  fouriersw  37978  fouriercn  37979  etransclem4  37986  etransclem7  37989  etransclem23  38005  etransclem24  38006  etransclem25  38007  etransclem26  38008  etransclem31  38013  etransclem32  38014  etransclem35  38017  etransclem37  38019  etransclem46  38028  sge0tsms  38073  sge0xaddlem2  38127  1t10e1p1e11  38523  deccarry  38528  1fzopredsuc  38534  m1mod0mod1  38536  iccpartgt  38554  m1expevenALTV  38590  1oddALTV  38632  6even  38651  8even  38653  gbpart7  38681  gbpart9  38683  gbpart11  38684  bgoldbtbndlem1  38713  tgoldbachlt  38722  3exp4mod41  38729  41prothprmlem1  38730  41prothprmlem2  38731  41prothprm  38732  pfxccatin12  38779  subsubmgm  39388  altgsumbcALT  39727  lincfsuppcl  39799  linccl  39800  lincvalsn  39803  lincdifsn  39810  lincsum  39815  lincscm  39816  lindslinindimp2lem4  39847  lindslinindsimp2lem5  39848  snlindsntor  39857  lincresunit3lem2  39866  zlmodzxzldeplem3  39888  ldepsnlinc  39894  nn0o1gt2  39920  nn0o  39922  nn0sumshdiglemA  40023  nn0sumshdiglemB  40024  sinh-conventional  40052  onetansqsecsq  40074  cotsqcscsq  40075  dpfrac1  40085  mvlraddi  40097  mvrladdi  40099  mvrraddi  40101  mvlrmuli  40109
  Copyright terms: Public domain W3C validator