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

Theorem oveq1i 6292
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 6289 . 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 1379  (class class class)co 6282
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-iota 5549  df-fv 5594  df-ov 6285
This theorem is referenced by:  caov12  6485  caov411  6489  omopthlem1  7301  map1  7591  pw2eng  7620  fsuppunbi  7846  cnfcomlem  8139  cnfcom2  8142  cnfcomlemOLD  8147  cnfcom2OLD  8150  infxpenc2  8395  infxpenc2OLD  8399  adderpqlem  9328  addassnq  9332  distrnq  9335  halfnq  9350  archnq  9354  addclprlem2  9391  addcmpblnr  9442  ltsrpr  9450  m1m1sr  9466  recexsrlem  9476  sqgt0sr  9479  map2psrpr  9483  axi2m1  9532  axcnre  9537  mul02lem2  9752  addid1  9755  cnegex2  9757  addid2  9758  mvlladdi  9833  negsubdi  9871  mulneg1  9989  recextlem1  10175  recdiv  10246  divmul13i  10301  mvllmuli  10373  2p2e4  10649  2times  10650  3p2e5  10664  3p3e6  10665  4p2e6  10666  4p3e7  10667  4p4e8  10668  5p2e7  10669  5p3e8  10670  5p4e9  10671  5p5e10  10672  6p2e8  10673  6p3e9  10674  6p4e10  10675  7p2e9  10676  7p3e10  10677  8p2e10  10678  1mhlfehlf  10754  8th4div3  10755  halfpm6th  10756  nneo  10940  uzindOLD  10951  num0h  10982  numsuc  10984  dec10p  11001  numma  11003  nummac  11004  numma2c  11005  numadd  11006  numaddc  11007  nummul2c  11009  decaddci  11017  decbin0  11075  decbin2  11076  xmulm1  11469  xadddi2  11485  x2times  11487  elfzp1b  11751  elfzm1b  11752  quoremz  11945  quoremnn0ALT  11947  uzrdgxfr  12040  mulexpz  12168  expaddz  12172  sqrecii  12212  cu2  12228  i3  12231  iexpcyc  12234  binom2i  12239  binom2aiOLD  12240  binom3  12249  crreczi  12253  discr  12265  nn0opthlem1  12310  nn0opth2i  12313  faclbnd  12330  bcm1k  12355  bcp1nk  12357  bcpasc  12361  hashp1i  12428  hashxplem  12451  hashpw  12454  hashfun  12455  hashbc  12462  ccatlid  12562  swrdccatin12  12673  revs1  12696  cats1cat  12783  imre  12898  crim  12905  remullem  12918  cnpart  13030  sqrtneglem  13057  absexpz  13095  absimle  13099  sqreulem  13148  amgm2  13158  iseraltlem2  13461  iseraltlem3  13462  modfsummod  13564  binomlem  13597  binom11  13600  arisum  13627  arisum2  13628  georeclim  13637  geo2sum  13638  mertenslem1  13649  mertens  13651  efzval  13691  resinval  13724  recosval  13725  efi4p  13726  tan0  13740  efival  13741  sinhval  13743  coshval  13744  cosadd  13754  cos2tsin  13768  ef01bndlem  13773  cos1bnd  13776  cos2bnd  13777  absefib  13787  efieq1re  13788  demoivreALT  13790  eirrlem  13791  rpnnen2lem3  13804  rpnnen2lem11  13812  ruclem7  13823  odd2np1  13898  3dvds  13902  divalglem2  13905  divalglem9  13911  m1bits  13942  sadcp1  13957  sadeq  13974  smupp1  13982  smumul  13995  gcdaddmlem  14018  nn0gcdsq  14137  phiprmpw  14158  prmdiv  14167  prmdiveq  14168  prmdivdiv  14169  pythagtriplem1  14192  pythagtriplem12  14202  pythagtriplem14  14204  pockthi  14277  infpnlem1  14280  prmreclem4  14289  4sqlem12  14326  4sqlem13  14327  4sqlem19  14333  vdwapun  14344  vdwlem6  14356  0hashbc  14377  dec5dvds  14402  dec5nprm  14404  dec2nprm  14405  modxai  14406  modxp1i  14408  mod2xnegi  14409  modsubi  14410  gcdmodi  14412  decexp2  14413  decsplit0b  14418  decsplit1  14420  decsplit  14421  karatsuba  14422  2exp6  14424  2exp8  14425  3exp3  14427  5prm  14445  7prm  14447  11prm  14451  prmlem2  14456  37prm  14457  43prm  14458  83prm  14459  139prm  14460  163prm  14461  317prm  14462  631prm  14463  1259lem1  14464  1259lem2  14465  1259lem3  14466  1259lem4  14467  1259lem5  14468  1259prm  14469  2503lem1  14470  2503lem2  14471  2503lem3  14472  2503prm  14473  4001lem1  14474  4001lem2  14475  4001lem3  14476  4001lem4  14477  4001prm  14478  pwsbas  14735  subsubc  15073  xpccatid  15308  subsubm  15795  mulg2  15948  subsubg  16016  oppgmnd  16181  gsumwrev  16193  psgnunilem2  16313  sylow1lem1  16411  subgslw  16429  sylow3  16446  efginvrel2  16538  efgsfo  16550  frgpnabllem1  16665  gsumzaddlem  16722  gsummptfzsplitl  16741  gsummpt1n0  16780  dprdfid  16844  ablfac1lem  16906  pgpfac1lem3  16915  pgpfaclem1  16919  mgpress  16939  srgbinomlem4  16979  opprrng  17061  unitsubm  17100  subsubrg  17235  lsslss  17387  evlsval  17956  mpff  17970  coe1fzgsumdlem  18111  evl1gsumdlem  18160  gzrngunit  18248  expghm  18293  expghmOLD  18294  chrid  18328  zrhpsgnmhm  18384  psgndiflemA  18401  frlmip  18573  frlmphl  18576  matvsca2  18694  mattposvs  18721  m2detleiblem3  18895  m2detleiblem4  18896  cpmidpmat  19138  resstopn  19450  cnmpt1res  19909  ressuss  20498  iscusp2  20537  ucnextcn  20539  txmetcnp  20782  rerest  21041  xrtgioo  21043  xrrest  21044  cnmpt2pc  21160  xrhmeo  21178  reust  21545  rrxprds  21553  csbren  21558  minveclem2  21573  ovolunlem1a  21639  ovolicc2lem4  21663  uniioombllem5  21728  iblabs  21967  iblabsr  21968  iblmulc2  21969  itgmulc2  21972  limcres  22022  dvfval  22033  dvreslem  22045  dvres2lem  22046  dvcnp2  22055  cpnres  22072  dvcobr  22081  dveflem  22112  lhop1lem  22146  lhop2  22148  dvcnvrelem2  22151  plyun0  22326  coeeulem  22353  coeeu  22354  dvply1  22411  dvtaylp  22496  taylthlem2  22500  taylth  22501  dvradcnv  22547  pserdvlem2  22554  abelthlem8  22565  abelth  22567  sinhalfpilem  22586  cospi  22595  eulerid  22597  cos2pi  22599  ef2kpi  22601  sinhalfpip  22615  sinhalfpim  22616  coshalfpip  22617  coshalfpim  22618  sincosq3sgn  22623  sincosq4sgn  22624  tangtx  22628  sincos4thpi  22636  sincos6thpi  22638  sineq0  22644  tanregt0  22656  logm1  22698  abslogle  22728  tanarg  22729  logcnlem4  22751  advlogexp  22761  cxpsqrt  22809  dvsqrt  22843  cxpcn3  22847  root1cj  22855  cxpeq  22856  ang180lem1  22866  ang180lem2  22867  ang180lem3  22868  lawcos  22873  isosctrlem1  22877  isosctrlem2  22878  quad2  22895  1cubrlem  22897  1cubr  22898  dcubic1lem  22899  dcubic2  22900  mcubic  22903  binom4  22906  dquartlem1  22907  quart1lem  22911  quart1  22912  quartlem1  22913  asinlem  22924  asinlem2  22925  asinlem3a  22926  acosneg  22943  efiasin  22944  asinsinlem  22947  asinsin  22948  acoscos  22949  asin1  22950  acosbnd  22956  atancj  22966  efiatan  22968  atanlogaddlem  22969  efiatan2  22973  2efiatan  22974  tanatan  22975  cosatan  22977  atantan  22979  atanbndlem  22981  atans2  22987  dvatan  22991  atantayl  22993  atantayl2  22994  log2cnv  23000  log2tlbnd  23001  log2ublem2  23003  log2ublem3  23004  log2ub  23005  birthday  23009  jensenlem1  23041  amgmlem  23044  wilthlem1  23067  ftalem2  23072  ftalem5  23075  ftalem6  23076  basellem2  23080  basellem3  23081  basellem5  23083  basellem8  23086  basellem9  23087  mule1  23147  ppi1i  23167  musum  23192  ppiublem1  23202  ppiublem2  23203  ppiub  23204  chtublem  23211  chtub  23212  dchrptlem1  23264  dchrptlem2  23265  bclbnd  23280  bpos1  23283  bposlem6  23289  bposlem8  23291  bposlem9  23292  lgslem4  23299  lgsdir2lem1  23323  lgsdir2lem2  23324  lgsdir2lem4  23326  lgsdir2lem5  23327  lgsne0  23333  1lgs  23337  lgseisenlem1  23349  lgseisenlem2  23350  lgseisenlem3  23351  lgseisenlem4  23352  lgseisen  23353  lgsquadlem1  23354  lgsquadlem2  23355  lgsquad2lem1  23358  lgsquad2lem2  23359  m1lgs  23362  chebbnd1lem2  23380  chebbnd1lem3  23381  rplogsumlem2  23395  dchrisum0flblem1  23418  dchrisum0re  23423  mulog2sumlem2  23445  chpdifbndlem1  23463  pntpbnd1a  23495  pntpbnd2  23497  pntibndlem2  23501  pntibndlem3  23502  pntlemg  23508  pntlemk  23516  pntlemo  23517  axsegconlem1  23893  ax5seglem7  23911  axlowdimlem3  23920  axlowdimlem16  23933  axlowdimlem17  23934  usgraexvlem  24068  fargshiftlem  24307  constr3trllem3  24325  eupares  24648  konigsberg  24660  numclwwlk5  24786  numclwwlk7  24788  frgraregord013  24792  ex-fl  24842  addinv  25027  vc2  25121  vc0  25135  vcm  25137  vcnegneg  25140  nvnncan  25231  nvm1  25240  nvpi  25242  nvmtri  25247  nvge0  25250  ipval3  25292  ipidsq  25296  ip0i  25413  ip1ilem  25414  ip2i  25416  ipdirilem  25417  ipasslem10  25427  siilem1  25439  siii  25441  minvecolem2  25464  hvsubid  25616  hvaddsubval  25623  hvmul2negi  25638  hvadd12i  25647  hv2times  25651  hvnegdii  25652  hvaddcani  25655  hi01  25686  hisubcomi  25694  normlem0  25699  normlem1  25700  normlem3  25702  normlem9  25708  bcseqi  25710  normsqi  25722  norm-ii-i  25727  normsubi  25731  norm3difi  25737  norm3adifii  25738  normpar2i  25746  polid2i  25747  polidi  25748  chdmm2i  26069  chj12i  26113  spanunsni  26170  qlaxr5i  26226  osumcor2i  26235  spansnji  26237  pjadjii  26265  pjinormii  26267  pjsslem  26270  pjpythi  26313  mayete3i  26319  mayete3iOLD  26320  mayetes3i  26321  hoadd12i  26369  honegneg  26398  ho2times  26411  hoaddsubi  26413  hosd1i  26414  hosd2i  26415  honpncani  26419  lnopeq0lem1  26597  lnopunilem1  26602  lnophmlem2  26609  lnfn0i  26634  nmopcoadji  26693  nmopcoadj2i  26694  opsqrlem1  26732  opsqrlem5  26736  opsqrlem6  26737  pjclem3  26789  stadd3i  26840  mddmd2  26901  mdexchi  26927  cvexchlem  26960  atomli  26974  atordi  26976  atabs2i  26994  mdsymlem1  26995  iuninc  27098  suppss3  27219  archirngz  27392  gsumvsca2  27434  nn0omnd  27491  nn0archi  27493  xrge0slmod  27494  sqsscirc1  27523  cnvordtrestixx  27528  raddcn  27544  xrge0iifhom  27552  xrge0mulc1cn  27556  xrge0tmd  27561  lmlimxrge0  27563  qqhucn  27606  rrhcn  27611  logb1  27656  brfae  27857  cndprobnul  28013  isrrvv  28019  ballotlem1  28062  ballotlem2  28064  ballotlemodife  28073  ballotlemi1  28078  ballotlemii  28079  ballotlemic  28082  ballotlem1c  28083  ballotlemfrceq  28104  ballotth  28113  ofcs2  28139  signsvtn0  28164  signstfveq0  28171  signsvtp  28177  signsvtn  28178  signsvfpn  28179  signsvfnn  28180  signshf  28182  lgamgulmlem2  28209  lgamgulmlem5  28212  lgambdd  28216  subfacp1lem1  28260  subfacp1lem5  28265  subfacp1lem6  28266  subfaclim  28269  cvmliftlem5  28371  cvmliftlem8  28374  cvmliftlem10  28376  cvmliftlem13  28378  cvmlift2lem6  28390  cvmlift2lem12  28396  problem1  28491  problem2  28492  problem4  28494  quad3  28496  prodfrec  28603  fprodm1s  28673  fprodp1s  28674  fallfacfwd  28732  0risefac  28734  bpolydiflem  29390  bpoly2  29393  bpoly3  29394  bpoly4  29395  fsumcube  29396  sin2h  29620  mblfinlem3  29628  ismblfin  29630  itg2addnclem3  29643  iblabsnc  29654  iblmulc2nc  29655  itgmulc2nc  29658  ftc1cnnc  29664  ftc1anclem6  29670  ftc1anclem7  29671  ftc1anclem8  29672  dvcnsqrt  29676  dvasin  29678  fdc  29839  heiborlem4  29911  heiborlem6  29913  pellexlem5  30371  reglog1  30434  jm2.23  30542  jm2.27c  30553  lnmlsslnm  30631  lmhmlnmsplit  30637  cntzsdrg  30756  areaquad  30789  hashnzfz2  30826  lhe4.4ex1a  30834  fzisoeu  31077  tgiooss  31110  constlimc  31166  sumnnodd  31172  limcresiooub  31184  limcresioolb  31185  cncfshiftioo  31231  fperdvper  31248  itgsinexplem1  31271  stoweidlem11  31311  stoweidlem13  31313  stoweidlem26  31326  stoweidlem34  31334  wallispilem4  31368  wallispi2lem1  31371  wallispi2lem2  31372  stirlinglem11  31384  dirkerper  31396  dirkertrigeqlem1  31398  dirkertrigeqlem3  31400  dirkercncflem1  31403  dirkercncflem4  31406  fourierdlem30  31437  fourierdlem32  31439  fourierdlem33  31440  fourierdlem42  31449  fourierdlem46  31453  fourierdlem47  31454  fourierdlem57  31464  fourierdlem60  31467  fourierdlem61  31468  fourierdlem62  31469  fourierdlem68  31475  fourierdlem73  31480  fourierdlem79  31486  fourierdlem89  31496  fourierdlem90  31497  fourierdlem91  31498  fourierdlem96  31503  fourierdlem97  31504  fourierdlem98  31505  fourierdlem99  31506  fourierdlem100  31507  fourierdlem103  31510  fourierdlem104  31511  fourierdlem108  31515  fourierdlem110  31517  fourierdlem113  31520  sqwvfoura  31529  sqwvfourb  31530  fourierswlem  31531  fouriersw  31532  fouriercn  31533  altgsumbcALT  32006  lincfsuppcl  32087  linccl  32088  lincvalsn  32091  lincdifsn  32098  lincsum  32103  lincscm  32104  lindslinindimp2lem4  32135  lindslinindsimp2lem5  32136  snlindsntor  32145  lincresunit3lem2  32154  zlmodzxzldeplem3  32184  ldepsnlinc  32190  sinh-conventional  32214  onetansqsecsq  32236  cotsqcscsq  32237  dpfrac1  32247  mvlraddi  32261  mvrladdi  32263  mvrraddi  32265  mvlrmuli  32273  sineq0ALT  32817  dalem24  34493  pmod2iN  34645  cdleme9  35049  cdleme20aN  35105  cdleme22e  35140  cdleme22eALTN  35141  cdleme25cv  35154  cdleme29b  35171  cdlemh1  35611  cdlemh2  35612  cdlemk35  35708  cdlemkid1  35718
  Copyright terms: Public domain W3C validator