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

Theorem reseq2i 5275
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 5273 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  |`cres 5006
This theorem is referenced by:  reseq12i  5276  rescom  5303  rescnvcnv  5475  resdm2  5502  funcnvres  5662  resasplit  5760  fresaunres2  5762  fresaunres1  5763  resdif  5841  resin  5842  fvn0ssdmfun  6022  residpr  6075  domss2  7696  ordtypelem1  7964  ackbij2lem3  8642  facnn  12355  fac0  12356  hashresfn  12413  ruclem4  13967  fsets  14658  setsid  14673  meet0  15767  join0  15768  symgfixelsi  16460  psgnsn  16545  dprd2da  17091  ply1plusgfvi  18283  uptx  20126  txcn  20127  ressxms  21028  ressms  21029  iscmet3lem3  21729  volres  21939  dvlip  22394  dvne0  22412  lhop  22417  dflog2  22948  dfrelog  22953  dvlog  23032  wilthlem2  23343  0pth  24572  2pthlem1  24597  ghsubgolemOLD  25372  zrdivrng  25434  df1stres  27522  df2ndres  27523  ffsrn  27552  resf1o  27553  fpwrelmapffs  27557  eulerpartlemn  28320  divcnvshft  29117  divcnvlin  29118  wfrlem5  29347  frrlem5  29391  isdrngo1  30359  eldioph4b  30745  diophren  30747  seff  31189  sblpnf  31190  radcnvrat  31195  hashnzfzclim  31227  dvresioo  31718  fourierdlem72  31961  fourierdlem80  31969  fourierdlem94  31983  fourierdlem103  31992  fourierdlem104  31993  fourierdlem113  32002  fouriersw  32014  rngcidOLD  32799  ringcidOLD  32862  bnj1326  34082
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482  df-opab 4511  df-xp 5010  df-res 5016
  Copyright terms: Public domain W3C validator