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

Theorem oveq1i 5884
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 5881 . 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 1632  (class class class)co 5874
This theorem is referenced by:  caov12  6064  caov411  6068  omopthlem1  6669  map1  6955  pw2eng  6984  cnfcomlem  7418  cnfcom2  7421  infxpenc2  7665  adderpqlem  8594  addassnq  8598  distrnq  8601  halfnq  8616  archnq  8620  addclprlem2  8657  addcmpblnr  8710  ltsrpr  8715  m1m1sr  8731  recexsrlem  8741  sqgt0sr  8744  map2psrpr  8748  axi2m1  8797  axcnre  8802  mul02lem2  9005  addid1  9008  cnegex2  9010  addid2  9011  negsubdi  9119  mulneg1  9232  recextlem1  9414  recdiv  9482  divmul13i  9537  2p2e4  9858  2times  9859  3p2e5  9871  3p3e6  9872  4p2e6  9873  4p3e7  9874  4p4e8  9875  5p2e7  9876  5p3e8  9877  5p4e9  9878  5p5e10  9879  6p2e8  9880  6p3e9  9881  6p4e10  9882  7p2e9  9883  7p3e10  9884  8p2e10  9885  1mhlfehlf  9950  8th4div3  9951  halfpm6th  9952  nneo  10111  uzindOLD  10122  num0h  10150  numsuc  10152  dec10p  10169  numma  10171  nummac  10172  numma2c  10173  numadd  10174  numaddc  10175  nummul2c  10177  decaddci  10185  decbin0  10243  decbin2  10244  xmulm1  10617  xadddi2  10633  x2times  10635  elfzm1b  10876  quoremz  10975  quoremnn0ALT  10977  uzrdgxfr  11045  mulexpz  11158  expaddz  11162  sqrecii  11202  cu2  11217  i3  11220  iexpcyc  11223  binom2i  11228  binom2aiOLD  11229  binom3  11238  crreczi  11242  discr  11254  nn0opthlem1  11299  nn0opth2i  11302  faclbnd  11319  bcm1k  11343  bcp1nk  11345  bcpasc  11349  hashp1i  11385  hashxplem  11401  hashpw  11404  hashfun  11405  hashbc  11407  ccatlid  11450  revs1  11499  cats1cat  11527  imre  11609  crim  11616  remullem  11629  cnpart  11741  sqrneglem  11768  absexpz  11806  absimle  11810  sqreulem  11859  amgm2  11869  iseraltlem2  12171  iseraltlem3  12172  binomlem  12303  binom11  12306  arisum  12334  arisum2  12335  georeclim  12344  geo2sum  12345  mertenslem1  12356  mertens  12358  ege2le3  12387  efzval  12398  resinval  12431  recosval  12432  efi4p  12433  tan0  12447  efival  12448  sinhval  12450  coshval  12451  cosadd  12461  cos2tsin  12475  ef01bndlem  12480  cos1bnd  12483  cos2bnd  12484  absefib  12494  efieq1re  12495  demoivreALT  12497  eirrlem  12498  rpnnen2lem3  12511  rpnnen2lem11  12519  ruclem7  12530  odd2np1  12603  3dvds  12607  divalglem2  12610  divalglem9  12616  m1bits  12647  sadcp1  12662  sadeq  12679  smupp1  12687  smumul  12700  gcdaddmlem  12723  nn0gcdsq  12839  phiprmpw  12860  prmdiv  12869  prmdiveq  12870  prmdivdiv  12871  pythagtriplem1  12885  pythagtriplem12  12895  pythagtriplem14  12897  pockthi  12970  infpnlem1  12973  prmreclem4  12982  4sqlem12  13019  4sqlem13  13020  4sqlem19  13026  vdwapun  13037  vdwlem6  13049  0hashbc  13070  dec5dvds  13095  dec5nprm  13097  dec2nprm  13098  modxai  13099  modxp1i  13101  mod2xnegi  13102  modsubi  13103  gcdmodi  13105  decexp2  13106  decsplit0b  13111  decsplit1  13113  decsplit  13114  karatsuba  13115  2exp6  13117  2exp8  13118  3exp3  13120  5prm  13126  7prm  13128  11prm  13132  prmlem2  13137  37prm  13138  43prm  13139  83prm  13140  139prm  13141  163prm  13142  317prm  13143  631prm  13144  1259lem1  13145  1259lem2  13146  1259lem3  13147  1259lem4  13148  1259lem5  13149  1259prm  13150  2503lem1  13151  2503lem2  13152  2503lem3  13153  2503prm  13154  4001lem1  13155  4001lem2  13156  4001lem3  13157  4001lem4  13158  4001prm  13159  pwsbas  13402  subsubc  13743  xpccatid  13978  subsubm  14450  mulg2  14592  subsubg  14656  oppgmnd  14843  gsumwrev  14855  sylow1lem1  14925  subgslw  14943  sylow3  14960  efginvrel2  15052  efgsfo  15064  frgpnabllem1  15177  ablfac1lem  15319  pgpfac1lem3  15328  pgpfaclem1  15332  mgpress  15352  opprrng  15429  unitsubm  15468  subsubrg  15587  lsslss  15734  gzrngunit  16453  expghm  16466  zrhval  16478  chrid  16497  resstopn  16932  cnmpt1res  17386  txmetcnp  18109  rerest  18326  xrtgioo  18328  xrrest  18329  cnmpt2pc  18442  xrhmeo  18460  minveclem2  18806  ovolunlem1a  18871  ovolicc2lem4  18895  uniioombllem5  18958  iblabs  19199  iblabsr  19200  iblmulc2  19201  itgmulc2  19204  limcres  19252  dvfval  19263  dvreslem  19275  dvres2lem  19276  dvcnp2  19285  cpnres  19302  dvcobr  19311  dveflem  19342  lhop1lem  19376  lhop2  19378  dvcnvrelem2  19381  evlsval  19419  mpff  19441  plyun0  19595  coeeulem  19622  coeeu  19623  dvply1  19680  dvtaylp  19765  taylthlem2  19769  taylth  19770  dvradcnv  19813  pserdvlem2  19820  abelthlem8  19831  abelth  19833  sinhalfpilem  19850  cospi  19856  eulerid  19858  cos2pi  19860  ef2kpi  19862  sinhalfpip  19876  sinhalfpim  19877  coshalfpip  19878  coshalfpim  19879  sincosq3sgn  19884  sincosq4sgn  19885  tangtx  19889  sincos4thpi  19897  sincos6thpi  19899  sineq0  19905  tanregt0  19917  logm1  19958  tanarg  19986  logcnlem4  20008  advlogexp  20018  cxpsqr  20066  dvsqr  20100  cxpcn3  20104  root1cj  20112  cxpeq  20113  ang180lem1  20123  ang180lem2  20124  ang180lem3  20125  lawcos  20130  isosctrlem1  20134  isosctrlem2  20135  quad2  20151  1cubrlem  20153  1cubr  20154  dcubic1lem  20155  dcubic2  20156  mcubic  20159  binom4  20162  dquartlem1  20163  quart1lem  20167  quart1  20168  quartlem1  20169  asinlem  20180  asinlem2  20181  asinlem3a  20182  acosneg  20199  efiasin  20200  asinsinlem  20203  asinsin  20204  acoscos  20205  asin1  20206  acosbnd  20212  atancj  20222  efiatan  20224  atanlogaddlem  20225  efiatan2  20229  2efiatan  20230  tanatan  20231  cosatan  20233  atantan  20235  atanbndlem  20237  atans2  20243  dvatan  20247  atantayl  20249  atantayl2  20250  log2cnv  20256  log2tlbnd  20257  log2ublem2  20259  log2ublem3  20260  log2ub  20261  birthday  20265  jensenlem1  20297  amgmlem  20300  wilthlem1  20322  ftalem2  20327  ftalem5  20330  ftalem6  20331  basellem2  20335  basellem3  20336  basellem5  20338  basellem8  20341  basellem9  20342  mule1  20402  ppi1i  20422  musum  20447  ppiublem1  20457  ppiublem2  20458  ppiub  20459  chtublem  20466  chtub  20467  dchrptlem1  20519  dchrptlem2  20520  bclbnd  20535  bpos1  20538  bposlem6  20544  bposlem8  20546  bposlem9  20547  lgslem4  20554  lgsdir2lem1  20578  lgsdir2lem2  20579  lgsdir2lem4  20581  lgsdir2lem5  20582  lgsne0  20588  1lgs  20592  lgseisenlem1  20604  lgseisenlem2  20605  lgseisenlem3  20606  lgseisenlem4  20607  lgseisen  20608  lgsquadlem1  20609  lgsquadlem2  20610  lgsquad2lem1  20613  lgsquad2lem2  20614  m1lgs  20617  chebbnd1lem2  20635  chebbnd1lem3  20636  rplogsumlem2  20650  dchrisum0flblem1  20673  dchrisum0re  20678  mulog2sumlem2  20700  chpdifbndlem1  20718  pntpbnd1a  20750  pntpbnd2  20752  pntibndlem2  20756  pntibndlem3  20757  pntlemg  20763  pntlemk  20771  pntlemo  20772  ex-fl  20850  addinv  21035  vc2  21127  vc0  21141  vcm  21143  vcnegneg  21146  nvnncan  21237  nvm1  21246  nvpi  21248  nvmtri  21253  nvge0  21256  ipval3  21298  ipidsq  21302  ip0i  21419  ip1ilem  21420  ip2i  21422  ipdirilem  21423  ipasslem10  21433  siilem1  21445  siii  21447  minvecolem2  21470  hvsubid  21621  hvaddsubval  21628  hvmul2negi  21643  hvadd12i  21652  hv2times  21656  hvnegdii  21657  hvaddcani  21660  hi01  21691  hisubcomi  21699  normlem0  21704  normlem1  21705  normlem3  21707  normlem9  21713  bcseqi  21715  normsqi  21727  norm-ii-i  21732  normsubi  21736  norm3difi  21742  norm3adifii  21743  normpar2i  21751  polid2i  21752  polidi  21753  chdmm2i  22073  chj12i  22117  spanunsni  22174  qlaxr5i  22230  osumcor2i  22239  spansnji  22241  pjadjii  22269  pjinormii  22271  pjsslem  22274  pjpythi  22317  mayete3i  22323  mayete3iOLD  22324  mayetes3i  22325  hoadd12i  22373  honegneg  22402  ho2times  22415  hoaddsubi  22417  hosd1i  22418  hosd2i  22419  honpncani  22423  lnopeq0lem1  22601  lnopunilem1  22606  lnophmlem2  22613  lnfn0i  22638  nmopcoadji  22697  nmopcoadj2i  22698  opsqrlem1  22736  opsqrlem5  22740  opsqrlem6  22741  pjclem3  22793  stadd3i  22844  mddmd2  22905  mdexchi  22931  cvexchlem  22964  atomli  22978  atordi  22980  atabs2i  22998  mdsymlem1  22999  ballotlem1  23061  ballotlem2  23063  ballotlemodife  23072  ballotlemi1  23077  ballotlemii  23078  ballotlemic  23081  ballotlem1c  23082  ballotlemfrceq  23103  ballotth  23112  iuninc  23174  sqsscirc1  23307  cnvordtrestixx  23312  raddcn  23317  xrge0iifhom  23334  xrge0mulc1cn  23338  xrge0tmd  23343  lmlimxrge0  23387  logb1  23420  cndprobnul  23655  isrrvv  23661  coinflippvt  23700  subfacp1lem1  23725  subfacp1lem5  23730  subfacp1lem6  23731  subfaclim  23734  cvmliftlem5  23835  cvmliftlem8  23838  cvmliftlem10  23840  cvmliftlem13  23842  cvmlift2lem6  23854  cvmlift2lem12  23860  eupares  23914  konigsberg  23926  elfzp1b  24027  faclimlem8  24124  faclim  24126  axsegconlem1  24617  ax5seglem7  24635  axlowdimlem3  24644  axlowdimlem16  24657  axlowdimlem17  24658  bpolydiflem  24861  bpoly2  24864  bpoly3  24865  bpoly4  24866  fsumcube  24867  itg2addnc  25005  iblabsnc  25015  iblmulc2nc  25016  itgmulc2nc  25019  ftc1cnnc  25025  3timesi  25281  fprodp1s  25430  vecax3  25558  islimrs  25683  cntrset  25705  cnegvex2  25763  1cat  25862  dualcat2  25887  indcls2  26099  fdc  26558  csbrn  26565  heiborlem4  26641  heiborlem6  26643  pellexlem5  27021  reglog1  27084  jm2.23  27192  jm2.27c  27203  lnmlsslnm  27282  lmhmlnmsplit  27288  psgnunilem2  27521  matvsca2  27581  cntzsdrg  27613  lhe4.4ex1a  27649  itgsinexplem1  27851  stoweidlem11  27863  stoweidlem13  27865  stoweidlem26  27878  stoweidlem34  27886  wallispilem4  27920  wallispi2lem1  27923  wallispi2lem2  27924  stirlinglem11  27936  usgraexvlem  28261  fargshiftlem  28379  constr3trllem3  28398  sinh-conventional  28463  onetansqsecsq  28485  cotsqcscsq  28486  dpfrac1  28496  dalem24  30508  pmod2iN  30660  cdleme9  31064  cdleme20aN  31120  cdleme22e  31155  cdleme22eALTN  31156  cdleme25cv  31169  cdleme29b  31186  cdlemh1  31626  cdlemh2  31627  cdlemk35  31723  cdlemkid1  31733
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279  df-ov 5877
  Copyright terms: Public domain W3C validator