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

Theorem reseq1i 5274
Description: Equality inference for restrictions. (Contributed by NM, 21-Oct-2014.)
Hypothesis
Ref Expression
reseqi.1
Assertion
Ref Expression
reseq1i

Proof of Theorem reseq1i
StepHypRef Expression
1 reseqi.1 . 2
2 reseq1 5272 . 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  resindm  5323  resmpt  5328  resmpt3  5329  opabresid  5332  rescnvcnv  5475  coires1  5530  fresaunres1  5763  fcoi1  5764  fninfp  6098  fvsnun1  6106  fvsnun2  6107  resoprab  6398  resmpt2  6400  elrnmpt2res  6416  ofmres  6796  f1stres  6822  f2ndres  6823  df1st2  6886  df2nd2  6887  dftpos2  6991  tfr2a  7083  tfr2b  7084  rdgseg  7107  frsucmpt2  7124  seqomlem2  7135  seqomlem3  7136  seqomlem4  7137  domss2  7696  dffi3  7911  fpwwe2lem13  9041  seqval  12118  hashgval  12408  hashinf  12410  pgrpsubgsymg  16433  gsumzunsnd  16982  ablfac1b  17121  zzngim  18591  pmatcollpw3lem  19284  cnmptid  20162  txflf  20507  xmsxmet2  20962  msmet2  20963  tmsxpsmopn  21040  isngp2  21117  subgnm  21147  tngngp2  21166  cnfldms  21283  msdcn  21346  oprpiece1res1  21451  oprpiece1res2  21452  cncms  21795  cnfldcusp  21797  reust  21813  minveclem3a  21842  dvreslem  22313  dvres2lem  22314  dvcmulf  22348  mdegfval  22460  psercn  22821  abelth  22836  efcvx  22844  efifo  22934  dfrelog  22953  dvrelog  23018  dvlog  23032  efopnlem2  23038  dvatan  23266  dchrisumlem1  23674  constr3pthlem1  24655  resmptf  27497  df1stres  27522  df2ndres  27523  ressplusf  27638  ressnm  27639  qqhcn  27972  cnrrext  27991  rrhre  27999  esumcvg  28092  dya2icoseg2  28249  eulerpartgbij  28311  trpred0  29319  wfrlem14  29356  mbfposadd  30062  ftc1anclem3  30092  dvasin  30103  dvacos  30104  neibastop2  30179  prdsbnd2  30291  repwsmet  30330  rrnequiv  30331  diophin  30706  eldioph4b  30745  dnnumch1  30990  aomclem6  31005  radcnvrat  31195  lhe4.4ex1a  31234  dvsid  31236  dvsef  31237  dvcosre  31706  dvmptresicc  31716  itgsinexplem1  31752  fourierdlem40  31929  fourierdlem57  31946  fourierdlem58  31947  fourierdlem62  31951  fourierdlem74  31963  fourierdlem75  31964  fourierdlem76  31965  fourierdlem80  31969  fourierdlem84  31973  fourierdlem85  31974  fourierdlem101  31990  fourierdlem102  31991  fourierdlem111  32000  fourierdlem114  32003  fouriersw  32014  fouriercn  32015  fdmdifeqresdif  32931  aacllem  33216
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-res 5016
  Copyright terms: Public domain W3C validator