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

Theorem reseq2i 5224
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 5222 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1370  |`cres 4959
This theorem is referenced by:  reseq12i  5225  rescom  5252  rescnvcnv  5420  resdm2  5447  funcnvres  5606  resasplit  5703  fresaunres2  5705  fresaunres1  5706  resdif  5783  resin  5784  residpr  6010  domss2  7604  ordtypelem1  7869  ackbij2lem3  8547  facnn  12210  fac0  12211  hashresfn  12268  ruclem4  13674  fsets  14358  setsid  14373  meet0  15466  join0  15467  symgfixelsi  16099  psgnsn  16185  dprd2da  16716  ply1plusgfvi  17877  uptx  19597  txcn  19598  ressxms  20499  ressms  20500  iscmet3lem3  21200  volres  21410  dvlip  21865  dvne0  21883  lhop  21888  dflog2  22412  dfrelog  22417  dvlog  22496  wilthlem2  22807  0pth  23938  2pthlem1  23963  ghsubgolem  24326  zrdivrng  24388  df1stres  26466  df2ndres  26467  ffsrn  26496  resf1o  26497  fpwrelmapffs  26501  eulerpartlemn  27220  divcnvshft  27854  divcnvlin  27855  wfrlem5  28184  frrlem5  28228  isdrngo1  29222  eldioph4b  29610  diophren  29612  seff  30055  sblpnf  30056  dvresioo  30480  fourierdlem72  30708  fourierdlem80  30716  fourierdlem94  30730  fourierdlem103  30739  fourierdlem104  30740  fourierdlem113  30749  fouriersw  30761  bnj1326  32860
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3083  df-in 3449  df-opab 4468  df-xp 4963  df-res 4969
  Copyright terms: Public domain W3C validator