Theorem resres 5291

Description: The restriction of a restriction. (Contributed by NM, 27-Mar-2008.)

Assertion

Ref	Expression
resres

Proof of Theorem resres

Step	Hyp	Ref	Expression
1		df-res 5016	. 2
2		df-res 5016	. . 3
3	2	ineq1i 3695	. 2
4		xpindir 5142	. . . 4
5	4	ineq2i 3696	. . 3
6		df-res 5016	. . 3
7		inass 3707	. . 3
8	5, 6, 7	3eqtr4ri 2497	. 2
9	1, 3, 8	3eqtri 2490	1

Syntax hints:  =wceq 1395  cvv 3109  i^icin 3474  X.cxp 5002  |`cres 5006

This theorem is referenced by:  rescom  5303  resabs1  5307  resima2  5312  resmpt3  5329  resdisj  5441  rescnvcnv  5475  fresin  5759  resdif  5841  curry1  6892  curry2  6895  pmresg  7466  gruima  9201  rlimres  13381  lo1res  13382  rlimresb  13388  lo1eq  13391  rlimeq  13392  fsets  14658  setsid  14673  sscres  15192  gsumzres  16914  gsumzresOLD  16918  txkgen  20153  tsmsresOLD  20645  tsmsres  20646  ressxms  21028  ressms  21029  dvres  22315  dvres3a  22318  cpnres  22340  dvmptres3  22359  rlimcnp2  23296  df1stres  27522  df2ndres  27523  indf1ofs  28039  wfrlem4  29346  frrlem4  29390  fouriersw  32014  fouriercn  32015

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-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  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-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-opab 4511  df-xp 5010  df-rel 5011  df-res 5016