Theorem reseq12d 5279

Description: Equality deduction for restrictions. (Contributed by NM, 21-Oct-2014.)

Hypotheses

Ref	Expression
reseqd.1
reseqd.2

Assertion

Ref	Expression
reseq12d

Proof of Theorem reseq12d

Step	Hyp	Ref	Expression
1		reseqd.1	. . 3
2	1	reseq1d 5277	. 2
3		reseqd.2	. . 3
4	3	reseq2d 5278	. 2
5	2, 4	eqtrd 2498	1

Syntax hints:  ->wi 4  =wceq 1395  |`cres 5006

This theorem is referenced by:  tfrlem3a  7065  oieq1  7958  oieq2  7959  ackbij2lem3  8642  setsvalg  14655  resfval  15261  resfval2  15262  resf2nd  15264  lubfval  15608  glbfval  15621  dpjfval  17104  psrval  18011  znval  18572  prdsdsf  20870  prdsxmet  20872  imasdsf1olem  20876  xpsxmetlem  20882  xpsmet  20885  isxms  20950  isms  20952  setsxms  20982  setsms  20983  ressxms  21028  ressms  21029  prdsxmslem2  21032  iscms  21784  cmsss  21789  minveclem3a  21842  dvcmulf  22348  efcvx  22844  ispth  24570  constr3pthlem1  24655  isrrext  27981  prdsbnd2  30291  cnpwstotbnd  30293  dvmptresicc  31716  itgcoscmulx  31768  fourierdlem73  31962  dfateq12d  32214  rngchomrnghmresOLD  32804  ldualset  34850

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