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

Theorem reseq2i 5078
Description: Equality inference for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypothesis
Ref Expression
reseqi.1
Assertion
Ref Expression
reseq2i

Proof of Theorem reseq2i
StepHypRef Expression
1 reseqi.1 . 2
2 reseq2 5076 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1687  |`cres 4813
This theorem is referenced by:  reseq12i  5079  rescom  5107  rescnvcnv  5273  resdm2  5300  funcnvres  5457  resasplit  5551  fresaunres2  5553  fresaunres1  5554  resdif  5631  resin  5632  residpr  5855  domss2  7429  ordtypelem1  7679  ackbij2lem3  8357  facnn  11994  fac0  11995  hashresfn  12052  ruclem4  13456  fsets  14140  setsid  14155  meet0  15247  join0  15248  symgfixelsi  15877  dprd2da  16409  ply1plusgfvi  17461  uptx  18902  txcn  18903  ressxms  19800  ressms  19801  iscmet3lem3  20501  volres  20711  dvlip  21165  dvne0  21183  lhop  21188  dflog2  21753  dfrelog  21758  dvlog  21837  wilthlem2  22148  0pth  23148  2pthlem1  23173  ghsubgolem  23536  zrdivrng  23598  df1stres  25679  df2ndres  25680  ffsrn  25709  resf1o  25710  fpwrelmapffs  25714  eulerpartlemn  26467  divcnvshft  27100  divcnvlin  27101  wfrlem5  27430  frrlem5  27474  isdrngo1  28433  eldioph4b  28823  diophren  28825  seff  29268  sblpnf  29269  bnj1326  31595
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403
This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-v 2953  df-in 3312  df-opab 4326  df-xp 4817  df-res 4823
  Copyright terms: Public domain W3C validator