Theorem resres 5142

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

Assertion

Ref	Expression
resres	|- ( ( A |` B ) |` C ) = ( A |` ( B i^i C ) )

Proof of Theorem resres

Step	Hyp	Ref	Expression
1		df-res 4871	. 2 |- ( ( A |` B ) |` C ) = ( ( A |` B ) i^i ( C X. _V ) )
2		df-res 4871	. . 3 |- ( A |` B ) = ( A i^i ( B X. _V ) )
3	2	ineq1i 3567	. 2 |- ( ( A |` B ) i^i ( C X. _V ) ) = ( ( A i^i ( B X. _V ) ) i^i ( C X. _V ) )
4		xpindir 4993	. . . 4 |- ( ( B i^i C ) X. _V ) = ( ( B X. _V ) i^i ( C X. _V ) )
5	4	ineq2i 3568	. . 3 |- ( A i^i ( ( B i^i C ) X. _V ) ) = ( A i^i ( ( B X. _V ) i^i ( C X. _V ) ) )
6		df-res 4871	. . 3 |- ( A |` ( B i^i C ) ) = ( A i^i ( ( B i^i C ) X. _V ) )
7		inass 3579	. . 3 |- ( ( A i^i ( B X. _V ) ) i^i ( C X. _V ) ) = ( A i^i ( ( B X. _V ) i^i ( C X. _V ) ) )
8	5, 6, 7	3eqtr4ri 2474	. 2 |- ( ( A i^i ( B X. _V ) ) i^i ( C X. _V ) ) = ( A |` ( B i^i C ) )
9	1, 3, 8	3eqtri 2467	1 |- ( ( A |` B ) |` C ) = ( A |` ( B i^i C ) )

Syntax hints:   = wceq 1369   _Vcvv 2991   i^i cin 3346   X. cxp 4857   |` cres 4861

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4432  ax-nul 4440  ax-pr 4550

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2739  df-rex 2740  df-rab 2743  df-v 2993  df-dif 3350  df-un 3352  df-in 3354  df-ss 3361  df-nul 3657  df-if 3811  df-sn 3897  df-pr 3899  df-op 3903  df-opab 4370  df-xp 4865  df-rel 4866  df-res 4871

This theorem is referenced by:  rescom  5154  resabs1  5158  resima2  5162  resmpt3  5176  resdisj  5286  rescnvcnv  5320  fresin  5599  resdif  5680  curry1  6683  curry2  6686  pmresg  7259  gruima  8988  rlimres  13055  lo1res  13056  rlimresb  13062  lo1eq  13065  rlimeq  13066  fsets  14219  setsid  14234  sscres  14755  gsumzres  16407  gsumzresOLD  16411  txkgen  19244  tsmsresOLD  19736  tsmsres  19737  ressxms  20119  ressms  20120  dvres  21405  dvres3a  21408  cpnres  21430  dvmptres3  21449  rlimcnp2  22379  df1stres  26018  df2ndres  26019  indf1ofs  26501  wfrlem4  27746  frrlem4  27790