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

Theorem oveq1i 5868
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 5865 . 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 1623  (class class class)co 5858
This theorem is referenced by:  caov12  6048  caov411  6052  omopthlem1  6653  map1  6939  pw2eng  6968  cnfcomlem  7402  cnfcom2  7405  infxpenc2  7649  adderpqlem  8578  addassnq  8582  distrnq  8585  halfnq  8600  archnq  8604  addclprlem2  8641  addcmpblnr  8694  ltsrpr  8699  m1m1sr  8715  recexsrlem  8725  sqgt0sr  8728  map2psrpr  8732  axi2m1  8781  axcnre  8786  mul02lem2  8989  addid1  8992  cnegex2  8994  addid2  8995  negsubdi  9103  mulneg1  9216  recextlem1  9398  recdiv  9466  divmul13i  9521  2p2e4  9842  2times  9843  3p2e5  9855  3p3e6  9856  4p2e6  9857  4p3e7  9858  4p4e8  9859  5p2e7  9860  5p3e8  9861  5p4e9  9862  5p5e10  9863  6p2e8  9864  6p3e9  9865  6p4e10  9866  7p2e9  9867  7p3e10  9868  8p2e10  9869  1mhlfehlf  9934  8th4div3  9935  halfpm6th  9936  nneo  10095  uzindOLD  10106  num0h  10134  numsuc  10136  dec10p  10153  numma  10155  nummac  10156  numma2c  10157  numadd  10158  numaddc  10159  nummul2c  10161  decaddci  10169  decbin0  10227  decbin2  10228  xmulm1  10601  xadddi2  10617  x2times  10619  elfzm1b  10860  quoremz  10959  quoremnn0ALT  10961  uzrdgxfr  11029  mulexpz  11142  expaddz  11146  sqrecii  11186  cu2  11201  i3  11204  iexpcyc  11207  binom2i  11212  binom2aiOLD  11213  binom3  11222  crreczi  11226  discr  11238  nn0opthlem1  11283  nn0opth2i  11286  faclbnd  11303  bcm1k  11327  bcp1nk  11329  bcpasc  11333  hashp1i  11369  hashxplem  11385  hashpw  11388  hashfun  11389  hashbc  11391  ccatlid  11434  revs1  11483  cats1cat  11511  imre  11593  crim  11600  remullem  11613  cnpart  11725  sqrneglem  11752  absexpz  11790  absimle  11794  sqreulem  11843  amgm2  11853  iseraltlem2  12155  iseraltlem3  12156  binomlem  12287  binom11  12290  arisum  12318  arisum2  12319  georeclim  12328  geo2sum  12329  mertenslem1  12340  mertens  12342  ege2le3  12371  efzval  12382  resinval  12415  recosval  12416  efi4p  12417  tan0  12431  efival  12432  sinhval  12434  coshval  12435  cosadd  12445  cos2tsin  12459  ef01bndlem  12464  cos1bnd  12467  cos2bnd  12468  absefib  12478  efieq1re  12479  demoivreALT  12481  eirrlem  12482  rpnnen2lem3  12495  rpnnen2lem11  12503  ruclem7  12514  odd2np1  12587  3dvds  12591  divalglem2  12594  divalglem9  12600  m1bits  12631  sadcp1  12646  sadeq  12663  smupp1  12671  smumul  12684  gcdaddmlem  12707  nn0gcdsq  12823  phiprmpw  12844  prmdiv  12853  prmdiveq  12854  prmdivdiv  12855  pythagtriplem1  12869  pythagtriplem12  12879  pythagtriplem14  12881  pockthi  12954  infpnlem1  12957  prmreclem4  12966  4sqlem12  13003  4sqlem13  13004  4sqlem19  13010  vdwapun  13021  vdwlem6  13033  0hashbc  13054  dec5dvds  13079  dec5nprm  13081  dec2nprm  13082  modxai  13083  modxp1i  13085  mod2xnegi  13086  modsubi  13087  gcdmodi  13089  decexp2  13090  decsplit0b  13095  decsplit1  13097  decsplit  13098  karatsuba  13099  2exp6  13101  2exp8  13102  3exp3  13104  5prm  13110  7prm  13112  11prm  13116  prmlem2  13121  37prm  13122  43prm  13123  83prm  13124  139prm  13125  163prm  13126  317prm  13127  631prm  13128  1259lem1  13129  1259lem2  13130  1259lem3  13131  1259lem4  13132  1259lem5  13133  1259prm  13134  2503lem1  13135  2503lem2  13136  2503lem3  13137  2503prm  13138  4001lem1  13139  4001lem2  13140  4001lem3  13141  4001lem4  13142  4001prm  13143  pwsbas  13386  subsubc  13727  xpccatid  13962  subsubm  14434  mulg2  14576  subsubg  14640  oppgmnd  14827  gsumwrev  14839  sylow1lem1  14909  subgslw  14927  sylow3  14944  efginvrel2  15036  efgsfo  15048  frgpnabllem1  15161  ablfac1lem  15303  pgpfac1lem3  15312  pgpfaclem1  15316  mgpress  15336  opprrng  15413  unitsubm  15452  subsubrg  15571  lsslss  15718  gzrngunit  16437  expghm  16450  zrhval  16462  chrid  16481  resstopn  16916  cnmpt1res  17370  txmetcnp  18093  rerest  18310  xrtgioo  18312  xrrest  18313  cnmpt2pc  18426  xrhmeo  18444  minveclem2  18790  ovolunlem1a  18855  ovolicc2lem4  18879  uniioombllem5  18942  iblabs  19183  iblabsr  19184  iblmulc2  19185  itgmulc2  19188  limcres  19236  dvfval  19247  dvreslem  19259  dvres2lem  19260  dvcnp2  19269  cpnres  19286  dvcobr  19295  dveflem  19326  lhop1lem  19360  lhop2  19362  dvcnvrelem2  19365  evlsval  19403  mpff  19425  plyun0  19579  coeeulem  19606  coeeu  19607  dvply1  19664  dvtaylp  19749  taylthlem2  19753  taylth  19754  dvradcnv  19797  pserdvlem2  19804  abelthlem8  19815  abelth  19817  sinhalfpilem  19834  cospi  19840  eulerid  19842  cos2pi  19844  ef2kpi  19846  sinhalfpip  19860  sinhalfpim  19861  coshalfpip  19862  coshalfpim  19863  sincosq3sgn  19868  sincosq4sgn  19869  tangtx  19873  sincos4thpi  19881  sincos6thpi  19883  sineq0  19889  tanregt0  19901  logm1  19942  tanarg  19970  logcnlem4  19992  advlogexp  20002  cxpsqr  20050  dvsqr  20084  cxpcn3  20088  root1cj  20096  cxpeq  20097  ang180lem1  20107  ang180lem2  20108  ang180lem3  20109  lawcos  20114  isosctrlem1  20118  isosctrlem2  20119  quad2  20135  1cubrlem  20137  1cubr  20138  dcubic1lem  20139  dcubic2  20140  mcubic  20143  binom4  20146  dquartlem1  20147  quart1lem  20151  quart1  20152  quartlem1  20153  asinlem  20164  asinlem2  20165  asinlem3a  20166  acosneg  20183  efiasin  20184  asinsinlem  20187  asinsin  20188  acoscos  20189  asin1  20190  acosbnd  20196  atancj  20206  efiatan  20208  atanlogaddlem  20209  efiatan2  20213  2efiatan  20214  tanatan  20215  cosatan  20217  atantan  20219  atanbndlem  20221  atans2  20227  dvatan  20231  atantayl  20233  atantayl2  20234  log2cnv  20240  log2tlbnd  20241  log2ublem2  20243  log2ublem3  20244  log2ub  20245  birthday  20249  jensenlem1  20281  amgmlem  20284  wilthlem1  20306  ftalem2  20311  ftalem5  20314  ftalem6  20315  basellem2  20319  basellem3  20320  basellem5  20322  basellem8  20325  basellem9  20326  mule1  20386  ppi1i  20406  musum  20431  ppiublem1  20441  ppiublem2  20442  ppiub  20443  chtublem  20450  chtub  20451  dchrptlem1  20503  dchrptlem2  20504  bclbnd  20519  bpos1  20522  bposlem6  20528  bposlem8  20530  bposlem9  20531  lgslem4  20538  lgsdir2lem1  20562  lgsdir2lem2  20563  lgsdir2lem4  20565  lgsdir2lem5  20566  lgsne0  20572  1lgs  20576  lgseisenlem1  20588  lgseisenlem2  20589  lgseisenlem3  20590  lgseisenlem4  20591  lgseisen  20592  lgsquadlem1  20593  lgsquadlem2  20594  lgsquad2lem1  20597  lgsquad2lem2  20598  m1lgs  20601  chebbnd1lem2  20619  chebbnd1lem3  20620  rplogsumlem2  20634  dchrisum0flblem1  20657  dchrisum0re  20662  mulog2sumlem2  20684  chpdifbndlem1  20702  pntpbnd1a  20734  pntpbnd2  20736  pntibndlem2  20740  pntibndlem3  20741  pntlemg  20747  pntlemk  20755  pntlemo  20756  ex-fl  20834  addinv  21019  vc2  21111  vc0  21125  vcm  21127  vcnegneg  21130  nvnncan  21221  nvm1  21230  nvpi  21232  nvmtri  21237  nvge0  21240  ipval3  21282  ipidsq  21286  ip0i  21403  ip1ilem  21404  ip2i  21406  ipdirilem  21407  ipasslem10  21417  siilem1  21429  siii  21431  minvecolem2  21454  hvsubid  21605  hvaddsubval  21612  hvmul2negi  21627  hvadd12i  21636  hv2times  21640  hvnegdii  21641  hvaddcani  21644  hi01  21675  hisubcomi  21683  normlem0  21688  normlem1  21689  normlem3  21691  normlem9  21697  bcseqi  21699  normsqi  21711  norm-ii-i  21716  normsubi  21720  norm3difi  21726  norm3adifii  21727  normpar2i  21735  polid2i  21736  polidi  21737  chdmm2i  22057  chj12i  22101  spanunsni  22158  qlaxr5i  22214  osumcor2i  22223  spansnji  22225  pjadjii  22253  pjinormii  22255  pjsslem  22258  pjpythi  22301  mayete3i  22307  mayete3iOLD  22308  mayetes3i  22309  hoadd12i  22357  honegneg  22386  ho2times  22399  hoaddsubi  22401  hosd1i  22402  hosd2i  22403  honpncani  22407  lnopeq0lem1  22585  lnopunilem1  22590  lnophmlem2  22597  lnfn0i  22622  nmopcoadji  22681  nmopcoadj2i  22682  opsqrlem1  22720  opsqrlem5  22724  opsqrlem6  22725  pjclem3  22777  stadd3i  22828  mddmd2  22889  mdexchi  22915  cvexchlem  22948  atomli  22962  atordi  22964  atabs2i  22982  mdsymlem1  22983  ballotlem1  23045  ballotlem2  23047  ballotlemodife  23056  ballotlemi1  23061  ballotlemii  23062  ballotlemic  23065  ballotlem1c  23066  ballotlemfrceq  23087  ballotth  23096  iuninc  23158  sqsscirc1  23292  cnvordtrestixx  23297  raddcn  23302  xrge0iifhom  23319  xrge0mulc1cn  23323  xrge0tmd  23328  lmlimxrge0  23372  logb1  23405  cndprobnul  23640  isrrvv  23646  coinflippvt  23685  subfacp1lem1  23710  subfacp1lem5  23715  subfacp1lem6  23716  subfaclim  23719  cvmliftlem5  23820  cvmliftlem8  23823  cvmliftlem10  23825  cvmliftlem13  23827  cvmlift2lem6  23839  cvmlift2lem12  23845  eupares  23899  konigsberg  23911  elfzp1b  24012  axsegconlem1  24545  ax5seglem7  24563  axlowdimlem3  24572  axlowdimlem16  24585  axlowdimlem17  24586  bpolydiflem  24789  bpoly2  24792  bpoly3  24793  bpoly4  24794  fsumcube  24795  3timesi  25178  fprodp1s  25327  vecax3  25455  islimrs  25580  cntrset  25602  cnegvex2  25660  1cat  25759  dualcat2  25784  indcls2  25996  fdc  26455  csbrn  26462  heiborlem4  26538  heiborlem6  26540  pellexlem5  26918  reglog1  26981  jm2.23  27089  jm2.27c  27100  lnmlsslnm  27179  lmhmlnmsplit  27185  psgnunilem2  27418  matvsca2  27478  cntzsdrg  27510  lhe4.4ex1a  27546  itgsinexplem1  27748  stoweidlem11  27760  stoweidlem13  27762  stoweidlem26  27775  stoweidlem34  27783  wallispilem4  27817  wallispi2lem1  27820  wallispi2lem2  27821  stirlinglem11  27833  usgraexvlem  28127  sinh-conventional  28209  onetansqsecsq  28231  cotsqcscsq  28232  dpfrac1  28242  dalem24  29886  pmod2iN  30038  cdleme9  30442  cdleme20aN  30498  cdleme22e  30533  cdleme22eALTN  30534  cdleme25cv  30547  cdleme29b  30564  cdlemh1  31004  cdlemh2  31005  cdlemk35  31101  cdlemkid1  31111
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861
  Copyright terms: Public domain W3C validator