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

Theorem oveq1i 6091
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 6088 . 2  |-  ( A  =  B  ->  ( A F C )  =  ( B F C ) )
31, 2ax-mp 8 1  |-  ( A F C )  =  ( B F C )
Colors of variables: wff set class
Syntax hints:    = wceq 1652  (class class class)co 6081
This theorem is referenced by:  caov12  6275  caov411  6279  omopthlem1  6898  map1  7185  pw2eng  7214  cnfcomlem  7656  cnfcom2  7659  infxpenc2  7903  adderpqlem  8831  addassnq  8835  distrnq  8838  halfnq  8853  archnq  8857  addclprlem2  8894  addcmpblnr  8947  ltsrpr  8952  m1m1sr  8968  recexsrlem  8978  sqgt0sr  8981  map2psrpr  8985  axi2m1  9034  axcnre  9039  mul02lem2  9243  addid1  9246  cnegex2  9248  addid2  9249  negsubdi  9357  mulneg1  9470  recextlem1  9652  recdiv  9720  divmul13i  9775  2p2e4  10098  2times  10099  3p2e5  10111  3p3e6  10112  4p2e6  10113  4p3e7  10114  4p4e8  10115  5p2e7  10116  5p3e8  10117  5p4e9  10118  5p5e10  10119  6p2e8  10120  6p3e9  10121  6p4e10  10122  7p2e9  10123  7p3e10  10124  8p2e10  10125  1mhlfehlf  10190  8th4div3  10191  halfpm6th  10192  nneo  10353  uzindOLD  10364  num0h  10392  numsuc  10394  dec10p  10411  numma  10413  nummac  10414  numma2c  10415  numadd  10416  numaddc  10417  nummul2c  10419  decaddci  10427  decbin0  10485  decbin2  10486  xmulm1  10860  xadddi2  10876  x2times  10878  elfzm1b  11125  quoremz  11236  quoremnn0ALT  11238  uzrdgxfr  11306  mulexpz  11420  expaddz  11424  sqrecii  11464  cu2  11479  i3  11482  iexpcyc  11485  binom2i  11490  binom2aiOLD  11491  binom3  11500  crreczi  11504  discr  11516  nn0opthlem1  11561  nn0opth2i  11564  faclbnd  11581  bcm1k  11606  bcp1nk  11608  bcpasc  11612  hashp1i  11672  hashxplem  11696  hashpw  11699  hashfun  11700  hashbc  11702  ccatlid  11748  revs1  11797  cats1cat  11825  imre  11913  crim  11920  remullem  11933  cnpart  12045  sqrneglem  12072  absexpz  12110  absimle  12114  sqreulem  12163  amgm2  12173  iseraltlem2  12476  iseraltlem3  12477  binomlem  12608  binom11  12611  arisum  12639  arisum2  12640  georeclim  12649  geo2sum  12650  mertenslem1  12661  mertens  12663  efzval  12703  resinval  12736  recosval  12737  efi4p  12738  tan0  12752  efival  12753  sinhval  12755  coshval  12756  cosadd  12766  cos2tsin  12780  ef01bndlem  12785  cos1bnd  12788  cos2bnd  12789  absefib  12799  efieq1re  12800  demoivreALT  12802  eirrlem  12803  rpnnen2lem3  12816  rpnnen2lem11  12824  ruclem7  12835  odd2np1  12908  3dvds  12912  divalglem2  12915  divalglem9  12921  m1bits  12952  sadcp1  12967  sadeq  12984  smupp1  12992  smumul  13005  gcdaddmlem  13028  nn0gcdsq  13144  phiprmpw  13165  prmdiv  13174  prmdiveq  13175  prmdivdiv  13176  pythagtriplem1  13190  pythagtriplem12  13200  pythagtriplem14  13202  pockthi  13275  infpnlem1  13278  prmreclem4  13287  4sqlem12  13324  4sqlem13  13325  4sqlem19  13331  vdwapun  13342  vdwlem6  13354  0hashbc  13375  dec5dvds  13400  dec5nprm  13402  dec2nprm  13403  modxai  13404  modxp1i  13406  mod2xnegi  13407  modsubi  13408  gcdmodi  13410  decexp2  13411  decsplit0b  13416  decsplit1  13418  decsplit  13419  karatsuba  13420  2exp6  13422  2exp8  13423  3exp3  13425  5prm  13431  7prm  13433  11prm  13437  prmlem2  13442  37prm  13443  43prm  13444  83prm  13445  139prm  13446  163prm  13447  317prm  13448  631prm  13449  1259lem1  13450  1259lem2  13451  1259lem3  13452  1259lem4  13453  1259lem5  13454  1259prm  13455  2503lem1  13456  2503lem2  13457  2503lem3  13458  2503prm  13459  4001lem1  13460  4001lem2  13461  4001lem3  13462  4001lem4  13463  4001prm  13464  pwsbas  13709  subsubc  14050  xpccatid  14285  subsubm  14757  mulg2  14899  subsubg  14963  oppgmnd  15150  gsumwrev  15162  sylow1lem1  15232  subgslw  15250  sylow3  15267  efginvrel2  15359  efgsfo  15371  frgpnabllem1  15484  ablfac1lem  15626  pgpfac1lem3  15635  pgpfaclem1  15639  mgpress  15659  opprrng  15736  unitsubm  15775  subsubrg  15894  lsslss  16037  gzrngunit  16764  expghm  16777  zrhval  16789  chrid  16808  resstopn  17250  cnmpt1res  17708  ressuss  18293  iscusp2  18332  ucnextcn  18334  txmetcnp  18577  rerest  18835  xrtgioo  18837  xrrest  18838  cnmpt2pc  18953  xrhmeo  18971  minveclem2  19327  ovolunlem1a  19392  ovolicc2lem4  19416  uniioombllem5  19479  iblabs  19720  iblabsr  19721  iblmulc2  19722  itgmulc2  19725  limcres  19773  dvfval  19784  dvreslem  19796  dvres2lem  19797  dvcnp2  19806  cpnres  19823  dvcobr  19832  dveflem  19863  lhop1lem  19897  lhop2  19899  dvcnvrelem2  19902  evlsval  19940  mpff  19962  plyun0  20116  coeeulem  20143  coeeu  20144  dvply1  20201  dvtaylp  20286  taylthlem2  20290  taylth  20291  dvradcnv  20337  pserdvlem2  20344  abelthlem8  20355  abelth  20357  sinhalfpilem  20374  cospi  20380  eulerid  20382  cos2pi  20384  ef2kpi  20386  sinhalfpip  20400  sinhalfpim  20401  coshalfpip  20402  coshalfpim  20403  sincosq3sgn  20408  sincosq4sgn  20409  tangtx  20413  sincos4thpi  20421  sincos6thpi  20423  sineq0  20429  tanregt0  20441  logm1  20483  abslogle  20513  tanarg  20514  logcnlem4  20536  advlogexp  20546  cxpsqr  20594  dvsqr  20628  cxpcn3  20632  root1cj  20640  cxpeq  20641  ang180lem1  20651  ang180lem2  20652  ang180lem3  20653  lawcos  20658  isosctrlem1  20662  isosctrlem2  20663  quad2  20679  1cubrlem  20681  1cubr  20682  dcubic1lem  20683  dcubic2  20684  mcubic  20687  binom4  20690  dquartlem1  20691  quart1lem  20695  quart1  20696  quartlem1  20697  asinlem  20708  asinlem2  20709  asinlem3a  20710  acosneg  20727  efiasin  20728  asinsinlem  20731  asinsin  20732  acoscos  20733  asin1  20734  acosbnd  20740  atancj  20750  efiatan  20752  atanlogaddlem  20753  efiatan2  20757  2efiatan  20758  tanatan  20759  cosatan  20761  atantan  20763  atanbndlem  20765  atans2  20771  dvatan  20775  atantayl  20777  atantayl2  20778  log2cnv  20784  log2tlbnd  20785  log2ublem2  20787  log2ublem3  20788  log2ub  20789  birthday  20793  jensenlem1  20825  amgmlem  20828  wilthlem1  20851  ftalem2  20856  ftalem5  20859  ftalem6  20860  basellem2  20864  basellem3  20865  basellem5  20867  basellem8  20870  basellem9  20871  mule1  20931  ppi1i  20951  musum  20976  ppiublem1  20986  ppiublem2  20987  ppiub  20988  chtublem  20995  chtub  20996  dchrptlem1  21048  dchrptlem2  21049  bclbnd  21064  bpos1  21067  bposlem6  21073  bposlem8  21075  bposlem9  21076  lgslem4  21083  lgsdir2lem1  21107  lgsdir2lem2  21108  lgsdir2lem4  21110  lgsdir2lem5  21111  lgsne0  21117  1lgs  21121  lgseisenlem1  21133  lgseisenlem2  21134  lgseisenlem3  21135  lgseisenlem4  21136  lgseisen  21137  lgsquadlem1  21138  lgsquadlem2  21139  lgsquad2lem1  21142  lgsquad2lem2  21143  m1lgs  21146  chebbnd1lem2  21164  chebbnd1lem3  21165  rplogsumlem2  21179  dchrisum0flblem1  21202  dchrisum0re  21207  mulog2sumlem2  21229  chpdifbndlem1  21247  pntpbnd1a  21279  pntpbnd2  21281  pntibndlem2  21285  pntibndlem3  21286  pntlemg  21292  pntlemk  21300  pntlemo  21301  usgraexvlem  21414  fargshiftlem  21621  constr3trllem3  21639  eupares  21697  konigsberg  21709  ex-fl  21755  addinv  21940  vc2  22034  vc0  22048  vcm  22050  vcnegneg  22053  nvnncan  22144  nvm1  22153  nvpi  22155  nvmtri  22160  nvge0  22163  ipval3  22205  ipidsq  22209  ip0i  22326  ip1ilem  22327  ip2i  22329  ipdirilem  22330  ipasslem10  22340  siilem1  22352  siii  22354  minvecolem2  22377  hvsubid  22528  hvaddsubval  22535  hvmul2negi  22550  hvadd12i  22559  hv2times  22563  hvnegdii  22564  hvaddcani  22567  hi01  22598  hisubcomi  22606  normlem0  22611  normlem1  22612  normlem3  22614  normlem9  22620  bcseqi  22622  normsqi  22634  norm-ii-i  22639  normsubi  22643  norm3difi  22649  norm3adifii  22650  normpar2i  22658  polid2i  22659  polidi  22660  chdmm2i  22980  chj12i  23024  spanunsni  23081  qlaxr5i  23137  osumcor2i  23146  spansnji  23148  pjadjii  23176  pjinormii  23178  pjsslem  23181  pjpythi  23224  mayete3i  23230  mayete3iOLD  23231  mayetes3i  23232  hoadd12i  23280  honegneg  23309  ho2times  23322  hoaddsubi  23324  hosd1i  23325  hosd2i  23326  honpncani  23330  lnopeq0lem1  23508  lnopunilem1  23513  lnophmlem2  23520  lnfn0i  23545  nmopcoadji  23604  nmopcoadj2i  23605  opsqrlem1  23643  opsqrlem5  23647  opsqrlem6  23648  pjclem3  23700  stadd3i  23751  mddmd2  23812  mdexchi  23838  cvexchlem  23871  atomli  23885  atordi  23887  atabs2i  23905  mdsymlem1  23906  iuninc  24011  sqsscirc1  24306  cnvordtrestixx  24311  raddcn  24315  xrge0iifhom  24323  xrge0mulc1cn  24327  xrge0tmd  24332  lmlimxrge0  24334  reust  24344  qqhucn  24376  rrhre  24387  logb1  24403  brfae  24599  cndprobnul  24695  isrrvv  24701  ballotlem1  24744  ballotlem2  24746  ballotlemodife  24755  ballotlemi1  24760  ballotlemii  24761  ballotlemic  24764  ballotlem1c  24765  ballotlemfrceq  24786  ballotth  24795  lgamgulmlem2  24814  lgamgulmlem5  24817  lgambdd  24821  subfacp1lem1  24865  subfacp1lem5  24870  subfacp1lem6  24871  subfaclim  24874  cvmliftlem5  24976  cvmliftlem8  24979  cvmliftlem10  24981  cvmliftlem13  24983  cvmlift2lem6  24995  cvmlift2lem12  25001  elfzp1b  25116  prodfrec  25223  fprodm1s  25293  fprodp1s  25294  fallfacfwd  25352  0risefac  25354  axsegconlem1  25856  ax5seglem7  25874  axlowdimlem3  25883  axlowdimlem16  25896  axlowdimlem17  25897  bpolydiflem  26100  bpoly2  26103  bpoly3  26104  bpoly4  26105  fsumcube  26106  mblfinlem3  26245  ismblfin  26247  itg2addnclem3  26258  iblabsnc  26269  iblmulc2nc  26270  itgmulc2nc  26273  ftc1cnnc  26279  ftc1anclem6  26285  ftc1anclem7  26286  ftc1anclem8  26287  fdc  26449  csbrn  26456  heiborlem4  26523  heiborlem6  26525  pellexlem5  26896  reglog1  26959  jm2.23  27067  jm2.27c  27078  lnmlsslnm  27156  lmhmlnmsplit  27162  psgnunilem2  27395  matvsca2  27455  cntzsdrg  27487  lhe4.4ex1a  27523  itgsinexplem1  27724  stoweidlem11  27736  stoweidlem13  27738  stoweidlem26  27751  stoweidlem34  27759  wallispilem4  27793  wallispi2lem1  27796  wallispi2lem2  27797  stirlinglem11  27809  swrdccatin12  28214  sinh-conventional  28482  onetansqsecsq  28504  cotsqcscsq  28505  dpfrac1  28515  sineq0ALT  29049  dalem24  30494  pmod2iN  30646  cdleme9  31050  cdleme20aN  31106  cdleme22e  31141  cdleme22eALTN  31142  cdleme25cv  31155  cdleme29b  31172  cdlemh1  31612  cdlemh2  31613  cdlemk35  31709  cdlemkid1  31719
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rex 2711  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-uni 4016  df-br 4213  df-iota 5418  df-fv 5462  df-ov 6084
  Copyright terms: Public domain W3C validator