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

Theorem oveq1i 6206
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 6203 . 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 1399  (class class class)co 6196
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-rex 2738  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-iota 5460  df-fv 5504  df-ov 6199
This theorem is referenced by:  caov12  6402  caov411  6406  omopthlem1  7222  map1  7513  pw2eng  7542  fsuppunbi  7765  cnfcomlem  8056  cnfcom2  8059  cnfcomlemOLD  8064  cnfcom2OLD  8067  infxpenc2  8312  infxpenc2OLD  8316  adderpqlem  9243  addassnq  9247  distrnq  9250  halfnq  9265  archnq  9269  addclprlem2  9306  addcmpblnr  9357  ltsrpr  9365  m1m1sr  9381  recexsrlem  9391  sqgt0sr  9394  map2psrpr  9398  axi2m1  9447  axcnre  9452  mul02lem2  9668  addid1  9671  cnegex2  9673  addid2  9674  mvlladdi  9750  negsubdi  9788  mulneg1  9911  recextlem1  10096  recdiv  10167  divmul13i  10222  mvllmuli  10294  2p2e4  10570  2times  10571  3p2e5  10585  3p3e6  10586  4p2e6  10587  4p3e7  10588  4p4e8  10589  5p2e7  10590  5p3e8  10591  5p4e9  10592  5p5e10  10593  6p2e8  10594  6p3e9  10595  6p4e10  10596  7p2e9  10597  7p3e10  10598  8p2e10  10599  1mhlfehlf  10675  8th4div3  10676  halfpm6th  10677  nneo  10863  num0h  10905  numsuc  10907  dec10p  10924  numma  10926  nummac  10927  numma2c  10928  numadd  10929  numaddc  10930  nummul2c  10932  decaddci  10940  decbin0  10998  decbin2  10999  xmulm1  11394  xadddi2  11410  x2times  11412  elfzp1b  11677  elfzm1b  11678  quoremz  11882  quoremnn0ALT  11884  uzrdgxfr  11980  mulexpz  12109  expaddz  12113  sqrecii  12153  cu2  12169  i3  12172  iexpcyc  12175  binom2i  12180  binom3  12189  crreczi  12193  discr  12205  nn0opthlem1  12250  nn0opth2i  12253  faclbnd  12270  bcm1k  12295  bcp1nk  12297  bcpasc  12301  hashp1i  12372  hashxplem  12395  hashpw  12398  hashfun  12399  hashbc  12406  ccatlid  12512  swrdccatin12  12627  revs1  12650  cats1cat  12737  imre  12943  crim  12950  remullem  12963  cnpart  13075  sqrtneglem  13102  absexpz  13140  absimle  13144  sqreulem  13194  amgm2  13204  iseraltlem2  13507  iseraltlem3  13508  modfsummod  13610  binomlem  13643  binom11  13646  arisum  13673  arisum2  13674  georeclim  13683  geo2sum  13684  mertenslem1  13695  mertens  13697  prodfrec  13706  fprodm1s  13776  fprodp1s  13777  efzval  13839  resinval  13872  recosval  13873  efi4p  13874  tan0  13888  efival  13889  sinhval  13891  coshval  13892  cosadd  13902  cos2tsin  13916  ef01bndlem  13921  cos1bnd  13924  cos2bnd  13925  absefib  13935  efieq1re  13936  demoivreALT  13938  eirrlem  13939  rpnnen2lem3  13952  rpnnen2lem11  13960  ruclem7  13971  odd2np1  14048  3dvds  14052  divalglem2  14055  divalglem9  14061  m1bits  14092  sadcp1  14107  sadeq  14124  smupp1  14132  smumul  14145  gcdaddmlem  14168  nn0gcdsq  14287  phiprmpw  14308  prmdiv  14317  prmdiveq  14318  prmdivdiv  14319  pythagtriplem1  14342  pythagtriplem12  14352  pythagtriplem14  14354  pockthi  14427  infpnlem1  14430  prmreclem4  14439  4sqlem12  14476  4sqlem13  14477  4sqlem19  14483  vdwapun  14494  vdwlem6  14506  0hashbc  14527  dec5dvds  14552  dec5nprm  14554  dec2nprm  14555  modxai  14556  modxp1i  14558  mod2xnegi  14559  modsubi  14560  gcdmodi  14562  decexp2  14563  decsplit0b  14568  decsplit1  14570  decsplit  14571  karatsuba  14572  2exp6OLD  14575  2exp8  14576  3exp3  14578  5prm  14596  7prm  14598  11prm  14602  prmlem2  14607  37prm  14608  43prm  14609  83prm  14610  139prm  14611  163prm  14612  317prm  14613  631prm  14614  1259lem1  14615  1259lem2  14616  1259lem3  14617  1259lem4  14618  1259lem5  14619  1259prm  14620  2503lem1  14621  2503lem2  14622  2503lem3  14623  2503prm  14624  4001lem1  14625  4001lem2  14626  4001lem3  14627  4001lem4  14628  4001prm  14629  pwsbas  14894  rcaninv  15200  subsubc  15259  xpccatid  15574  subsubm  16105  mulg2  16268  subsubg  16341  oppgmnd  16506  gsumwrev  16518  psgnunilem2  16637  sylow1lem1  16735  subgslw  16753  sylow3  16770  efginvrel2  16862  efgsfo  16874  frgpnabllem1  16994  gsumzaddlem  17051  gsummptfzsplitl  17069  gsummpt1n0  17106  dprdfid  17170  ablfac1lem  17232  pgpfac1lem3  17241  pgpfaclem1  17245  mgpress  17265  srgbinomlem4  17307  opprring  17393  unitsubm  17432  subsubrg  17568  lsslss  17720  evlsval  18301  mpff  18315  coe1fzgsumdlem  18456  evl1gsumdlem  18505  xrsnsgrp  18567  gzrngunit  18596  expghm  18626  chrid  18657  zrhpsgnmhm  18711  psgndiflemA  18728  frlmip  18898  frlmphl  18901  matvsca2  19015  mattposvs  19042  m2detleiblem3  19216  m2detleiblem4  19217  cpmidpmat  19459  resstopn  19773  cnmpt1res  20262  ressuss  20851  iscusp2  20890  ucnextcn  20892  txmetcnp  21135  rerest  21394  xrtgioo  21396  xrrest  21397  cnmpt2pc  21513  xrhmeo  21531  reust  21898  rrxprds  21906  csbren  21911  minveclem2  21926  ovolunlem1a  21992  ovolicc2lem4  22016  uniioombllem5  22081  iblabs  22320  iblabsr  22321  iblmulc2  22322  itgmulc2  22325  limcres  22375  dvfval  22386  dvreslem  22398  dvres2lem  22399  dvcnp2  22408  cpnres  22425  dvcobr  22434  dveflem  22465  lhop1lem  22499  lhop2  22501  dvcnvrelem2  22504  plyun0  22679  coeeulem  22706  coeeu  22707  dvply1  22765  dvtaylp  22850  taylthlem2  22854  taylth  22855  dvradcnv  22901  pserdvlem2  22908  abelthlem8  22919  abelth  22921  sinhalfpilem  22941  cospi  22950  eulerid  22952  cos2pi  22954  ef2kpi  22956  sinhalfpip  22970  sinhalfpim  22971  coshalfpip  22972  coshalfpim  22973  sincosq3sgn  22978  sincosq4sgn  22979  tangtx  22983  sincos4thpi  22991  sincos6thpi  22993  sineq0  22999  tanregt0  23011  logm1  23061  abslogle  23090  tanarg  23091  logcnlem4  23113  advlogexp  23123  cxpsqrt  23171  dvsqrt  23205  cxpcn3  23209  root1cj  23217  cxpeq  23218  logb1  23227  ang180lem1  23259  ang180lem2  23260  ang180lem3  23261  lawcos  23266  isosctrlem1  23268  isosctrlem2  23269  quad2  23286  1cubrlem  23288  1cubr  23289  dcubic1lem  23290  dcubic2  23291  mcubic  23294  binom4  23297  dquartlem1  23298  quart1lem  23302  quart1  23303  quartlem1  23304  asinlem  23315  asinlem2  23316  asinlem3a  23317  acosneg  23334  efiasin  23335  asinsinlem  23338  asinsin  23339  acoscos  23340  asin1  23341  acosbnd  23347  atancj  23357  efiatan  23359  atanlogaddlem  23360  efiatan2  23364  2efiatan  23365  tanatan  23366  cosatan  23368  atantan  23370  atanbndlem  23372  atans2  23378  dvatan  23382  atantayl  23384  atantayl2  23385  log2cnv  23391  log2tlbnd  23392  log2ublem2  23394  log2ublem3  23395  log2ub  23396  birthday  23401  jensenlem1  23433  amgmlem  23436  wilthlem1  23459  ftalem2  23464  ftalem5  23467  ftalem6  23468  basellem2  23472  basellem3  23473  basellem5  23475  basellem8  23478  basellem9  23479  mule1  23539  ppi1i  23559  musum  23584  ppiublem1  23594  ppiublem2  23595  ppiub  23596  chtublem  23603  chtub  23604  dchrptlem1  23656  dchrptlem2  23657  bclbnd  23672  bpos1  23675  bposlem6  23681  bposlem8  23683  bposlem9  23684  lgslem4  23691  lgsdir2lem1  23715  lgsdir2lem2  23716  lgsdir2lem4  23718  lgsdir2lem5  23719  lgsne0  23725  1lgs  23729  lgseisenlem1  23741  lgseisenlem2  23742  lgseisenlem3  23743  lgseisenlem4  23744  lgseisen  23745  lgsquadlem1  23746  lgsquadlem2  23747  lgsquad2lem1  23750  lgsquad2lem2  23751  m1lgs  23754  chebbnd1lem2  23772  chebbnd1lem3  23773  rplogsumlem2  23787  dchrisum0flblem1  23810  dchrisum0re  23815  mulog2sumlem2  23837  chpdifbndlem1  23855  pntpbnd1a  23887  pntpbnd2  23889  pntibndlem2  23893  pntibndlem3  23894  pntlemg  23900  pntlemk  23908  pntlemo  23909  axsegconlem1  24341  ax5seglem7  24359  axlowdimlem3  24368  axlowdimlem16  24381  axlowdimlem17  24382  usgraexvlem  24516  fargshiftlem  24755  constr3trllem3  24773  eupares  25096  konigsberg  25108  numclwwlk5  25233  numclwwlk7  25235  frgraregord013  25239  ex-fl  25289  ex-ind-dvds  25291  addinv  25471  vc2  25565  vc0  25579  vcm  25581  vcnegneg  25584  nvnncan  25675  nvm1  25684  nvpi  25686  nvmtri  25691  nvge0  25694  ipval3  25736  ipidsq  25740  ip0i  25857  ip1ilem  25858  ip2i  25860  ipdirilem  25861  ipasslem10  25871  siilem1  25883  siii  25885  minvecolem2  25908  hvsubid  26060  hvaddsubval  26067  hvmul2negi  26082  hvadd12i  26091  hv2times  26095  hvnegdii  26096  hvaddcani  26099  hi01  26130  hisubcomi  26138  normlem0  26143  normlem1  26144  normlem3  26146  normlem9  26152  bcseqi  26154  normsqi  26166  norm-ii-i  26171  normsubi  26175  norm3difi  26181  norm3adifii  26182  normpar2i  26190  polid2i  26191  polidi  26192  chdmm2i  26513  chj12i  26557  spanunsni  26614  qlaxr5i  26670  osumcor2i  26679  spansnji  26681  pjadjii  26709  pjinormii  26711  pjsslem  26714  pjpythi  26757  mayete3i  26763  mayetes3i  26764  hoadd12i  26812  honegneg  26841  ho2times  26854  hoaddsubi  26856  hosd1i  26857  hosd2i  26858  honpncani  26862  lnopeq0lem1  27040  lnopunilem1  27045  lnophmlem2  27052  lnfn0i  27077  nmopcoadji  27136  nmopcoadj2i  27137  opsqrlem1  27175  opsqrlem5  27179  opsqrlem6  27180  pjclem3  27232  stadd3i  27283  mddmd2  27344  mdexchi  27370  cvexchlem  27403  atomli  27417  atordi  27419  atabs2i  27437  mdsymlem1  27438  iuninc  27557  suppss3  27700  archirngz  27886  gsumvsca2  27928  nn0omnd  27985  nn0archi  27987  xrge0slmod  27988  sqsscirc1  28044  cnvordtrestixx  28049  raddcn  28065  xrge0iifhom  28073  xrge0mulc1cn  28077  xrge0tmd  28082  lmlimxrge0  28084  qqhucn  28126  rrhcn  28131  brfae  28376  inelcarsg  28438  cndprobnul  28559  isrrvv  28565  ballotlem1  28608  ballotlem2  28610  ballotlemodife  28619  ballotlemi1  28624  ballotlemii  28625  ballotlemic  28628  ballotlem1c  28629  ballotlemfrceq  28650  ballotth  28659  ofcs2  28685  signsvtn0  28710  signstfveq0  28717  signsvtp  28723  signsvtn  28724  signsvfpn  28725  signsvfnn  28726  signshf  28728  lgamgulmlem2  28761  lgamgulmlem5  28764  lgambdd  28768  subfacp1lem1  28812  subfacp1lem5  28817  subfacp1lem6  28818  subfaclim  28821  cvmliftlem5  28923  cvmliftlem8  28926  cvmliftlem10  28928  cvmliftlem13  28930  cvmlift2lem6  28942  cvmlift2lem12  28948  problem1  29208  problem2  29209  problem4  29211  quad3  29213  iexpire  29288  fallfacfwd  29324  0risefac  29326  bpolydiflem  29969  bpoly2  29972  bpoly3  29973  bpoly4  29974  fsumcube  29975  sin2h  30210  mblfinlem3  30218  ismblfin  30220  itg2addnclem3  30234  iblabsnc  30245  iblmulc2nc  30246  itgmulc2nc  30249  ftc1cnnc  30255  ftc1anclem6  30261  ftc1anclem7  30262  ftc1anclem8  30263  dvcnsqrt  30267  dvasin  30269  fdc  30404  heiborlem4  30476  heiborlem6  30478  pellexlem5  30934  reglog1  30997  jm2.23  31104  jm2.27c  31115  lnmlsslnm  31193  lmhmlnmsplit  31199  cntzsdrg  31319  areaquad  31352  hashnzfz2  31394  lhe4.4ex1a  31402  binomcxplemdvsum  31428  binomcxplemnotnn0  31429  binomcxp  31430  fzisoeu  31666  fz1ssfz0  31676  fsummulc1f  31735  fprodexp  31766  constlimc  31796  sumnnodd  31802  limcresiooub  31814  limcresioolb  31815  cncfshiftioo  31861  fperdvper  31881  dvnmul  31906  dvmptfprod  31908  itgsinexplem1  31918  stoweidlem11  31959  stoweidlem13  31961  stoweidlem26  31974  stoweidlem34  31982  wallispilem4  32016  wallispi2lem1  32019  wallispi2lem2  32020  stirlinglem11  32032  dirkerper  32044  dirkertrigeqlem1  32046  dirkertrigeqlem3  32048  dirkercncflem1  32051  dirkercncflem4  32054  fourierdlem30  32085  fourierdlem32  32087  fourierdlem33  32088  fourierdlem42  32097  fourierdlem46  32101  fourierdlem47  32102  fourierdlem57  32112  fourierdlem60  32115  fourierdlem61  32116  fourierdlem62  32117  fourierdlem68  32123  fourierdlem73  32128  fourierdlem79  32134  fourierdlem89  32144  fourierdlem90  32145  fourierdlem91  32146  fourierdlem96  32151  fourierdlem97  32152  fourierdlem98  32153  fourierdlem99  32154  fourierdlem100  32155  fourierdlem103  32158  fourierdlem104  32159  fourierdlem108  32163  fourierdlem110  32165  fourierdlem113  32168  sqwvfoura  32177  sqwvfourb  32178  fourierswlem  32179  fouriersw  32180  fouriercn  32181  etransclem4  32187  etransclem7  32190  etransclem23  32206  etransclem24  32207  etransclem25  32208  etransclem26  32209  etransclem31  32214  etransclem32  32215  etransclem35  32218  etransclem37  32220  etransclem46  32229  m1mod0mod1  32460  m1expevenALTV  32490  1oddALTV  32532  3exp4mod41  32550  41prothprmlem1  32551  41prothprmlem2  32552  41prothprm  32553  pfxccatin12  32600  subsubmgm  32803  altgsumbcALT  33142  lincfsuppcl  33214  linccl  33215  lincvalsn  33218  lincdifsn  33225  lincsum  33230  lincscm  33231  lindslinindimp2lem4  33262  lindslinindsimp2lem5  33263  snlindsntor  33272  lincresunit3lem2  33281  zlmodzxzldeplem3  33303  ldepsnlinc  33309  nn0o1gt2  33337  nn0o  33339  nn0sumshdiglemA  33440  nn0sumshdiglemB  33441  sinh-conventional  33469  onetansqsecsq  33491  cotsqcscsq  33492  dpfrac1  33502  mvlraddi  33514  mvrladdi  33516  mvrraddi  33518  mvlrmuli  33526  sineq0ALT  34084  dalem24  35834  pmod2iN  35986  cdleme9  36391  cdleme20aN  36448  cdleme22e  36483  cdleme22eALTN  36484  cdleme25cv  36497  cdleme29b  36514  cdlemh1  36954  cdlemh2  36955  cdlemk35  37051  cdlemkid1  37061  cotrclrcl  38250  inductionexd  38496
  Copyright terms: Public domain W3C validator